leanprover
feat: indent on enter after certain EOL tokens
This PR causes indentation when hitting enter after certain tokens that appear at the end of a line. Specifically, after:
by,do,try,finally,then,else,where,extends,deriving,:=,=>, and<|
It also inserts two indentations in the case that we hit enter immediately after : on a line that doesn't start with a binder bracket. We exclude binder-bracket-initial lines so as to avoid inserting improper indentation after already-indented hypotheses:
theorem foo (...)
(...) :| <-- hit enter here
| <-- cursor ends up here
If we encounter one of the "postindented EOL tokens" or a trailing : in the first line of a focus block, we add extra indentation as appropriate.
- [ ] depends on: #328
Ideally, we'd be able to describe indentation using Lean's parser, as an autoformatter implemented by the extension would.
Currently, this adds extra indents (after the first) by appending \t. ~~I'm not sure if VS code can be asked to indent twice "natively" in this situation, and I'm not sure if using \t would be problematic when it comes to distinctions between space-based indents and tab-based indents.~~ It seems that VS code converts these to spaces as appropriate, and cannot be asked to indent multiple times any other way.
This PR is WIP; please feel free to comment with any opinions or suggestions, especially if I've missed any common tokens! :)
(I haven't forgotten this PR and I'll get back to re-reviewing it as soon as I find time for it)
After mulling on this PR for a while, I think that there are unfortunately too many edge cases where the post-indented EOL token heuristics do the wrong thing. I'm afraid that accidentally adding incorrect indentation on occasion is much more annoying than consistently not adding any additional indentation, so I would prefer to not add these rules.
I've thought a bit about whether there is a better way to add these rules than the one in this PR, but I can't think of any with the limited view of the text that VS Code gives us with this configuration option.
Makes sense! (I wish VS code would let us access the result of parsing somehow...)
Just to be clear, do you consider adding some indentation but not enough indentation to be part of the issue, or is the problem only the potential for "overshooting"? If the latter, I think there are some tokens which are always followed by at least one postindentation (such as try), for which we could develop rules that never overshoot. (We could also restrict to different circumstances to avoid overshooting, such as "by when the line starts with no whitespace and a def-like token".) (We'd want to verify any such universal style claims with regexes on mathlib before committing to them, of course.)
But, I undertand if you feel that adding some-but-not-necessarily-enough indentation causes more cognitive overhead than simply not doing so at all. :)
Makes sense! (I wish VS code would let us access the result of parsing somehow...)
There's the textDocument/onTypeFormatting request, but the central problem is that you need to elaborate all dependencies of a declaration in order to be able to parse it, and so the latency for this request can be unacceptably high (think trying to use auto-completion in a portion of the document where the orange bars haven't disappeared yet). Hence, this approach unfortunately isn't really feasible for us, either.
Just to be clear, do you consider adding some indentation but not enough indentation to be part of the issue, or is the problem only the potential for "overshooting"?
I consider inconsistent behavior in general to be bad and especially bad w.r.t. something that you usually don't need to think about, like input. In this context, I'd say that inconsistently adding too much indentation is worse than inconsistently adding too little indentation, because having to actively revert something that the computer did incorrectly is always extra frustrating (compared to needing to help it along).
Specifically, I don't see a way that we can handle multi-line function signatures correctly in a way that doesn't overshoot or undershoot, and I think that this specific inconsistency will be sufficiently frustrating in practice (in either direction) that it's probably better to err on the side of simple indentation inheritance.