search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
267 stars 70 forks source link

Trim left whitespace from Idris add-clause response #590

Closed keram closed 1 year ago

keram commented 1 year ago

Why: Idris2 returns generated string with indentation and as we compute the indentation ourself the result ends inserted with extra space.

Before change result of idris-add-clause on indented block in Idris2 before-change-indent-add-clause

After change after-change-indent-add-clause

(no change Idris1)