Highlight some text while hoverTooltip is activated

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?

1 Like

That sounds OK!

This patch (released with @codemirror/view 6.30.0) adds a feature for that.

3 Likes

it works very good in my case, Thank you, Marijn!

Have a nice day!