fix: improve syntax precision for start of #doc blocks#771
fix: improve syntax precision for start of #doc blocks#771ejgallego wants to merge 2 commits intoleanprover:mainfrom
Conversation
As of today, we used a synthetic placeholder for title syntax. This confused the LSP extension as it overgeralized the start of the span, which after the TOC-merge phase made the entry to appear as the parents of all other entries, for example existing declarations.
robsimmons
left a comment
robsimmons
left a comment
There was a problem hiding this comment.
Heck yes. I wonder if there are reasons where/why it would be helpful to track the location of the #doc tag itself?
Indeed I wonder what'd be best here. I just had a look at the test output and indeed it still looks a bit suspicious. Would love to pair and brainstorm any time on this! |
| [{"selectionRange": | ||
| {"start": {"line": 0, "character": 0}, "end": {"line": 0, "character": 12}}, | ||
| "range": | ||
| {"start": {"line": 0, "character": 0}, "end": {"line": 11, "character": 0}}, |
There was a problem hiding this comment.
The start here looks wrong. Let me look into it.
There was a problem hiding this comment.
Tried a fix but introduced a LSP violation (selectionRange not within range, see below)
| # Docs heading | ||
| Text | ||
| ::::::: | ||
| --^ textDocument/documentSymbol |
There was a problem hiding this comment.
Not sure this call is worth the effort, I'll keep it as a witness of the non-incrementality of documentSymbol
|
Preview for this PR is ready! 🎉 |
| {"selectionRange": | ||
| {"start": {"line": 26, "character": 0}, "end": {"line": 33, "character": 7}}, | ||
| "range": | ||
| {"start": {"line": 26, "character": 0}, "end": {"line": 33, "character": 0}}, |
There was a problem hiding this comment.
There is a violation of the LSP spec here, selectionRange must be contained in range.
Working on a fix.
There was a problem hiding this comment.
Seems like we should fix that. Do you plan to do that in this PR?
There was a problem hiding this comment.
Yes, the fix turned out to be more involved than I wanted, due to header{} being a synthetic token, which actually made the headings not carry location and not appear on the outline view.
There was a problem hiding this comment.
This is indeed a serious violation, so I'll add a panic for this problem. In this case the origin of the issue was a little typo in the code getPos vs getTailPos.
It's certainly useful for giving a good outline view and for populating the declaration ranges table. |
| splits the logic in this function across multiple functions. | ||
| -/ | ||
| private meta def elabDoc (genre: Term) (title: StrLit) (topLevelBlocks : Array Syntax) (endPos: String.Pos.Raw) : TermElabM Term := do | ||
| private meta def elabDoc (rootStx : Syntax) (genre: Term) (title: StrLit) (topLevelBlocks : Array Syntax) (endPos: String.Pos.Raw) : TermElabM Term := do |
There was a problem hiding this comment.
The meaning of rootStx isn't particularly apparent to me when just reading here. How about explaining in the docstring that it's the syntax of the complete #doc ... => line?
There was a problem hiding this comment.
We might also want to call it ref for consistency with Lean internals if you think that makes sense
There was a problem hiding this comment.
Or could we drop the parameter and just call getRef here?
There was a problem hiding this comment.
I'll find a better name, I agree.
Let me look into using getRef, as of now, in working branch, I'm doing a little bit of surgery but I agree it'd be better if we could use getRef.
3 participants
As of today, we used a synthetic placeholder for title syntax. This confused the LSP extension as it overgeralized the start of the span, which after the TOC-merge phase made the entry to appear as the parents of all other entries, for example existing declarations.