don't recompile when typing space at EOL

Stream: lean4

[Floris van Doorn]

I don't know how feasible this is, but it would be nice if a proof doesn't recompile if you write a space at the end of a line. This is a common occurrence, since you often need to type spaces to go to the correct indentation to and see the goal state.

Of course, a much more ambitious "don't re-elaborate if the output of the parser didn't change in relevant ways" would be better, but that sounds a lot trickier (e.g. we still want to update the line/column numbers of everything). This might be a much simpler and very common case.