LSP code folding support #1014
LSP code folding support #1014
Conversation
The following constructs are foldable: - Sections and namespaces - Blocks of import/open statements - Multi-line commands (so mostly definitions) - Mutual definitions - Module-level doc comments - Top-level definition doc comments Fixes #1012
| let ⟨snaps, e?⟩ ← doc.allSnaps.updateFinishedPrefix | ||
| let mut stxs := snaps.finishedPrefix.map (·.stx) | ||
| match e? with | ||
| | some ElabTaskError.aborted => | ||
| throw RequestError.fileChanged | ||
| | some (ElabTaskError.ioError e) => | ||
| throw (e : RequestError) | ||
| | _ => pure () | ||
|
|
||
| let lastSnap := snaps.finishedPrefix.getLastD doc.headerSnap | ||
| stxs := stxs ++ (← parseAhead doc.meta.text.source lastSnap).toList |
There was a problem hiding this comment.
This is copied from handleDocumentSymbol, right? Let's put that in a new function... hmm... getDocumentSyntaxWithParseAhead?
There was a problem hiding this comment.
After some proper dogfooding of this branch, I'm not actually sure doing a parse ahead is the right choice here. I've had a couple of times when the a newly opened file has somewhat incorrect folding regions, I assume due to the parseahead being a little inaccurate.
I think there's a couple of options here:
- Do what semantic highlighting does, and wait for all tasks to complete. It's means that folding regions will be a little slow to appear, though maybe that's not the end of the world.
- Add support for LSP's partial results, and stream regions as each snapshot finishes. Obviously much more complex, as we'd need to handle editors which don't support partial results.
There was a problem hiding this comment.
Interesting, inaccurate in what way?
as we'd need to handle editors which don't support partial results
Which is all of them, unfortunately
There was a problem hiding this comment.
Interesting, inaccurate in what way?
There were a couple of times where only part of an inductive type was picked up (so some constructors were inside the folding region and some weren't). I'm afraid I didn't look into it too much at the time - will have a bit more of a poke.
Which is all of them, unfortunately
Oh, that is unfortunate. I had thought (hoped) that they'd made their way into the standard as VS Code needed/wanted them.
There was a problem hiding this comment.
Here is a relatively minimal case where parse-ahead fails. I can only reproduce when running under a debug build, though I imagine the same would happen with a release build if you had a term which takes sufficiently long to elaborate.
def foo :=
0
infixl:65 " :=: " => Eq
theorem bar : 0 :=: 0 :=
rflEditing the definition of foo will result in only foo having a folding region as, I assume, infixl hasn't been processed and so the definition of bar doesn't parse. I don't think there's much that can really be done about this :(.
- Wait for all terms to be elaborated before showing folding regions. May want to change this to support partial results. - Use .span to extract import statements, rather than mutually recursive functions. - Some tiny other bits of cleanup
|
Sorry about the delay, I lost track of this PR. I see you've since updated it to wait for elaboration, so given that we do this for other requests such as semantic highlighting as well, I think this is good to go! |
This adds code folding support to the language server (see #1012), making the following constructs foldable:
Example: Screenshot of VS Code with the test file open, and the folding handles visible.
Afraid I've not used Lean for a few years now (and obviously this was Lean 3), so sure I've made some mistakes. I'm not especially happy with how doc-comments are handled - don't know if there's a better way of poking the syntax?