I’m working on a CM6 based web editor for Lean4, it runs LSP in server to respond the semantic queries.
I want to support LSP hover in CM, so I used the hoverTooltip plugin, it sends the LSP textDocument/hover request and show a tooltip for it, that’s good.
However, LSP server will also return a range object, which represents user-focused semantic object, I want to highlight the text in range during the hover tooltip. Is there a good way to do it? Thanks!
This is currently difficult to do, since you cannot really recognize the transactions that open or close a hover tooltip. Would a feature that gives you access to the state field storing the active tooltips produced by the hover tooltip, which you could wire up to EditorView.decorations.compute, solve this problem for you?
That sounds OK!
This patch (released with @codemirror/view 6.30.0) adds a feature for that.
it works very good in my case, Thank you, Marijn!
Have a nice day!