[CatarinaGamboa]

Closes #197

What changes

The editor hover shows a LiquidJava error as one markdown card: VS Code's own problem part holds only the title (it renders that message as plain text), and the extension's markdown part under it holds the headline, the origin notes, the counterexample and the hints:

• code the verifier marks with backticks is inline code (editor font), without the backticks;
• each line reference (line 134) is a link that opens that file at that line, from the structured references (SourceReferenceDTO), not a text search;
• hints get a Hint / Hints heading, as in the panel, and several call sequences are listed under "Any one of these:";
• everything else is escaped, so *, _, <, |, # in expressions stay literal.

In the LiquidJava view, the code in the Origin line and in the hints gets the look of inline code in a markdown hover (textCodeBlock.background, inherited colour) instead of the preformatted-text colours, which drew grey boxes around it in light themes.

Before this PR, the hints were not in the editor hover at all, and the notes and counterexample were plain text with raw backticks.

Server: the diagnostic message is the title alone (LJDiagnosticsHandler.diagnosticMessage). This is what the Problems tab, F8 and the squiggle show; the headline, the notes and the counterexample are in the hover's card and in the view.

Shared parsing. The code-span and reference parsing that #193 wrote for the panel moves from webview/message-text.ts to utils/message-text.ts (splitMessageText, no vscode import, so both bundles use it). The panel renders the segments as HTML, the hover as markdown (utils/message-markdown.ts, formatDiagnosticMarkdown). The grouping of call sequences into options (groupHints) moves there too.

Trust. The links are file: URIs with an #L<line>,<col> fragment, which VS Code opens without a command, so the markdown part is not trusted (no isTrusted, no command links). The existing refinement hover keeps its own trusted MarkdownString; the diagnostic card is a separate part of the hover.

Design choice

VS Code's diagnostic hover is always plain text, and the same string is the Problems tab entry. Rendering the headline in markdown without showing it twice means the diagnostic itself carries only the title, so the Problems tab and the problem view (F8) show the error type, not the headline (screenshot below). The PM chose the card over the Problems tab text (2026-11-11); putting Title: headline back in the diagnostic is a one-line change in diagnosticMessage if that is ever wanted.

Screenshots

Headless VS Code (openvscode 1.109), verifier 0.0.38, study task A1_38, cursor on the error. Before = main + the first version of this PR (hints only); after = this PR.

	Before	After
Hover, dark
Hover, light
Problems tab, dark	(headline + notes + counterexample as plain text)
View, dark
View, light

The first version's screenshots (hints only, E_A3_07 with a clickable line 51, A1_09 with two call sequences) are in the PR's history under pr-screenshots/197/*-after.png and *-link.png.

Not in this PR

• The squiggle's range ends one character before the LiquidJava position (getRangeFromPosition uses endColumn - 1), so on the last character of the error our part shows without the problem part. Pre-existing; left alone.
• Line tags (x@51) in the hover's code are shown as the verifier writes them; Render the verifier's line tags as subscripts and name every part of an error alike #196 renders them as subscripts in the panel only.

Tests

• utils/message-markdown.spec.ts: code spans incl. a multi-backtick and a padded span, the link at the reference's start, escaping of * < _ | #; call sequences as options; a diagnostic's headline, then notes, then counterexample, then hints; the headline alone when it has nothing else.
• LJDiagnosticsHandlerTest: the diagnostic's message is the title alone.
• Client: npm run test:unit (140 passed), npm run test:typecheck, npm run lint, npx tsc --noEmit. Server: mvn -B test -Dtest=LJDiagnosticsHandlerTest.
• Rebased on main (after Render the verifier's line tags as subscripts and name every part of an error alike #196); the conflict in webview/message-text.ts resolved as described in the overlap note of the first version.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1 (codex exec review --base origin/main, gpt-6-sol, medium)

No actionable regression was identified in the diff. Type-checking and all unit tests pass.

No findings, so no further rounds.

[CatarinaGamboa]

Clean-code audit (SOLID / DRY / KISS) of this PR's diff

• utils/message-text.ts - [core-dry] The backtick and reference parsing exists once, shared by the panel (HTML) and the hover (markdown). The call-sequence grouping is shared too, so the two surfaces cannot drift.
• utils/message-markdown.ts - [solid-dip] The link builder is passed in (LinkTarget), so the module has no vscode import and is unit-tested without the editor. hover.ts passes vscode.Uri.
• services/hover.ts toLocationLink - [core-dry] The method hover's "Go to Refinements Definition" link and the hint links build the file:…#L<line>,<col> URI in one place now.
• services/hover.ts getHoveredHints - [solid-srp] Selecting the diagnostics at the cursor stays in the hover provider; formatting stays in the pure module. It does not reuse updateErrorAtCursor (context.ts), which answers a different question: which refinement error is in scope before the cursor, not which diagnostic covers it.
• [core-kiss] There is no command, and markdown trust is not changed. The hint part is untrusted, and file: links open without a command.
• utils/message-text.ts:20 - [core-kiss] Minor: the flushText closure gathers plain characters into one segment. A per-character segment would need merging later, so it stays.

Nothing to change.

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main on 9b6502c. One finding.

• [P2] Show hover details for diagnostics without a source position (client/src/services/hover.ts): "When a diagnostic has no source position, the server still publishes a native diagnostic at (0,0), but this filter excludes its custom diagnostic entirely. Because the patch removes notes and counterexamples from the native message, those details, and any hints, are no longer available in the editor hover for that case."

Declined. A diagnostic without a position has no file either, and getDiagnostics groups it under PathUtils.toFileUri(null), which is the empty URI, so no native diagnostic is shown for it in any editor; there is no hover to add a part to. It is listed in the LiquidJava view (Workspace), with its notes and hints, as before. The notes were never visible in a hover for that case, so the PR takes nothing away there.

Nothing else reported.

[CatarinaGamboa]

Clean-code review

Audit of this PR's own diff with the clean-code-principles checklist.

• Fixed server/src/main/java/LJDiagnosticsHandler.java [name-meaningful]: getHoverMessage renamed diagnosticMessage; since this PR it is the text of the Problems tab and the problem view as much as of the hover.
• Noted, not changed server/src/main/java/LJDiagnosticsHandler.java [core-dry]: plainCode repeats the verifier's code-span rule (liquidjava.diagnostics.Code: the fence, the one space of padding), which utils/message-text.ts repeats on the client as well. The verifier's Code.render is colour-only and its plain variant is package-private, so the server cannot call it; a Code.plain(String) in the verifier would remove the Java copy, but that is a verifier release, not this PR.
• client/src/utils/message-markdown.ts: formatHintsMarkdown stays exported for its tests only; kept, since the tests are the PR's.

Nothing else: the hover, the markdown formatter and the HTML renderer each keep one job, and the parser they share has one home (utils/message-text.ts).

[CatarinaGamboa]

Round 2 (acbeda2): the headline is in the markdown card as well, with its code as inline code; the diagnostic itself now carries only the title, so the Problems tab and F8 show the error type (screenshot row added to the description). Hover and Problems screenshots in the description are from this build, dark and light.