insertion of several new lines at once extremely slow

[gh-salt]

When pressing Enter continuously to insert several new lines, the insertion is extremelly slow. It seems to be due to the need to refresh the position of the cursor for each inserted line so it is probably linked with automatic indentation.

[m-fleury]

Work-around: C-j (line break without indenting)

The deep problem here is that the indentation is non-local. To indent a given line, you need to go back to the previous line that starts with a command.

What does that mean? Well assume you start with

lemma True
  by auto

and insert 10 lines afterwards. Each time, emacs moves the cursor back to by auto to know how deep it should be indented, yielding roughly ~55 cursor moves.

I have to implement some sort of caching. I will try to understand how other modes are doing it…