You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Render hints as markdown in the editor hover: code spans and line links #197
Impact: since verifier 0.0.38 the hints mark code with backticks (Call `open()` first) and name lines (line 42). The Verification panel renders both (#193), but the editor hover and the Problems tab show the diagnostic as plain text, so users see raw backticks and an unclickable "line 42" in the place they look first.
To do:
Render the hints in the editor hover as markdown: code spans in the editor font, and each line reference as a link that opens that line (the references the server already sends, SourceReferenceDTO).
VS Code's own diagnostic hover is always plain text, so this needs the extension's hover (client/src/services/hover.ts already returns a MarkdownString), shown over the error range. Decide how it sits next to VS Code's plain diagnostic hover without repeating the same text twice (e.g. a shorter diagnostic message plus the full markdown hover, or the hints only in ours).
Escape everything that is not a code span or a link, since hints can contain *, _, < or | from expressions.
Probably the message notes too (From/Origin), which use the same backticks and line names; check that it does not make the hover too long at the study's width.
The Problems tab stays plain text; copy-diagnostic keeps the ASCII form.
Prior work: a local prototype from #192, proto/192-markdown-hover (899c93d, "markdown hover for the notes and counterexample, not for merge"), adds client/src/services/diagnostic-hover.ts.
Activity
Screenshots for #197