[CatarinaGamboa]

Closes #192

Stacked on #191 (base feat/181-declaration-notes): it renders #191's declared-here gloss, and it needs the same 0.0.38 bump. Retarget this PR to main before #191 is merged with --delete-branch.

What changes

Server

• LJDiagnosticDTO now sends two more fields for every diagnostic:
  • messageNotes, from getMessageNotes();
  • references, from getReferences(), as SourceReferenceDTO(message, text, start, position). The position counts lines and columns from 0, like the other DTO positions.
• Both come from the verifier's generic LJDiagnostic API. New notes and references therefore show up with no extension change.

Panel (Verification tab)

• The message notes, e.g. Origin: line 134, …, are shown under Found and the Counterexample. Before this PR the panel did not show notes at all.
• Every message line goes through one renderer, webview/message-text.ts: the header message, notes, hints and the declared-here gloss.
  • Code the verifier marks with backticks is shown in the editor font, without the backticks, with VS Code's inline-code colours (textPreformat).
  • Spans are parsed as the verifier's Code.render parses them: the same run-of-backticks pattern, and one space of padding stripped.
• Each reference (line 134, ArrayListRefinements.java:162) is a link that opens that file at that line. It is placed at the reference's start; the text is not searched for, as the verifier asks. It reuses the panel's existing location-link handler.
• Hints are now in the UI font, so their code stands out. Before, the whole hint was monospace.
• Header message: it is now escaped. Before, it was put into the HTML unescaped.

Hover and Problems: unchanged by this PR. See the two options below.

Verifier version

Needs a release (0.0.38 or later) containing liquid-java/liquidjava#528, #530 and #533, on top of #517 and #525 (both on main).

• getReferences(), SourceReference and the backticks come from #533.
• The Origin notes come from #528/#530.

I tested against #533's head (1e94930), installed as 0.0.38 into an isolated Maven repository. Like #191, CI's server build fails until 0.0.38 is on Maven Central.

Panel at the study width: before (#191) → after (this PR)

Both use verifier #533, with Hints open. The notes are new, the code is set apart, and line 134 is a link.

A1_38	A2_10

A2_04	A1_56

A1_01	A1_09 (hints)

Clicking line 134 in A1_38 opens line 134, new BufferedInputStream(stream):

Panel text of the notes (verifier #533):

A1_38  Origin: line 134, new BufferedInputStream(stream) makes markState(buffered) == unmarked
A1_01  Origin: line 130, writer.getDefaultWriteParam() returns compression(wParam) == compressionNotExplicit
A2_04  Origin: line 94, timeout is a parameter of checkCimReachable(String, int) with no refinement
A2_10  Origin: ArrayListRefinements.java:162, failures.size() guarantees only failures.size() >= 0
A1_56  Origin: line 69, frame.getUndoManager() says nothing about redoState(undoManager)

A1_09 has no Origin note.

Hover: the two options

VS Code shows a diagnostic's message as plain text. So the diagnostic hover and the Problems view keep the backticks.

• A, plain text (Show the message notes and the counterexample in the hover #190): the diagnostic message is the headline, then the notes, then the counterexample, all plain with backticks, as rustc writes them. One text, the same as the CLI with colour off, in the hover and in Problems.
• B, markdown provider (prototype on branch proto/192-markdown-hover, not in this PR):
  • The diagnostic message stays the headline only, as on main.
  • The extension's HoverProvider adds a markdown block with the notes and the counterexample: code spans, and line 134 as a link.
  • VS Code draws it under the problem part, so nothing is shown twice. That holds only as long as Show the message notes and the counterexample in the hover #190's notes are not also in the diagnostic message.

	A: plain (#190 + #533)	B: markdown provider
A1_38
A2_04
A2_10
A1_01

Recommendation: A for the study.

• Same text everywhere. The hover is the one surface the baseline shares, and the joint review's decision 5 says compared elements must be in the hover/CLI text. A gives one string: hover = Problems = CLI with colour off.
• B splits the message. It shows the message in two hover parts with two styles: the headline plain with backticks, the notes styled. The Problems view also loses the notes.
• B reads better on its own: the code is set apart, and the cause is one click away. It is a good candidate after the study. Moving to it means taking the notes back out of Show the message notes and the counterexample in the hover #190's diagnostic message, so the two must not both be merged.

Overlap with open PRs

• Show every declared-here position and its gloss in the IDE panel #191: the base of this PR.
• Show the Context tab's refinements as the error messages show them #186 may conflict in sections.ts: both change the imports at the top.
• Wrap the Verification panel at spaces and operators, one conjunct per line #189 may conflict in errors.ts (imports, and next to the Expected lines) and in styles.ts (separate rules, so unlikely).
• List Found as facts and show only readable simplification steps #185: probably no textual conflict. It edits LJErrorDTO and the error types in types/diagnostics.ts; this PR edits LJDiagnosticDTO and BaseDiagnostic.
• Show the message notes and the counterexample in the hover #190: no conflict in files. It is option A of the hover (above).

Checks

npm run test:unit (126 passed; the new panel test fails on the base), npm run test:typecheck, npm run lint, server mvn -B test (40 passed, against #533 as 0.0.38; the new converter test fails on the base).

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

I audited this diff with the clean-code-principles checklist.

Fixed

• One renderer (renderMessageText) for every message line: header, notes, hints and gloss, instead of separate escaping at each place (DRY). It also fixes the unescaped header message.
• The references are matched by their start, not by searching the text, so the code cannot mislead the link.

Declined

• DRY: renderReferenceLink repeats the attributes of sections.ts's renderLocationLink. Reusing it would make message-text.ts import sections.ts, which imports message-text.ts, a circular import. It would also need a text parameter that renderLocationLink does not have.
• func-few-arguments: LJDiagnosticDTO's private constructor takes 9 fields. It mirrors the existing public one, which takes 7, so the explicit-value path (LJErrorDTO) stays unchanged.

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/feat/181-declaration-notes (this PR's own diff, since it is stacked on #191): "I found no actionable regressions in the diff. Client unit tests and type-checking pass; server tests could not run because Maven could not resolve the existing verifier dependency."

That is the unreleased 0.0.38, as stated in the body. Locally, the server tests pass (40) against #533 installed as 0.0.38 in an isolated Maven repository.

The loop ends here: nothing to fix.