[CatarinaGamboa]

Closes #181

What changes

• Server. RefinementErrorDTO and StateRefinementErrorDTO now send:

  • declarationPositions, from LJDiagnostic.getDeclarationPositions();
  • declarationNotes, the where … means … lines, from getDeclarationNotes().

  Both are read through the verifier's generic LJDiagnostic API. So when the verifier adds notes or positions, they appear with no extension change. declarationPosition, the first position, stays as it is for the State Machine view.

• Client. The Locations section links to every declaration position, then shows the notes under the links, muted and with a hanging indent. A declaration in value form (doorState(this) == closed), or one with unnamed sets, has no notes, so nothing changes for it.

• Fallback to one position. The verifier's default getDeclarationPositions() returns the single getDeclarationPosition(). Refinement errors and any other error with one declaration therefore show one link, as before.

Verifier version: needs 0.0.38 (not yet released)

Part	Verifier change
declarationNotes (the gloss)	liquid-java/liquidjava#517 (merged in main)
declarationPositions (every from, e.g. A1_01 lines 110 and 111)	liquid-java/liquidjava#525 (open)

The pom is bumped to 0.0.38, so CI's server build fails until 0.0.38 is on Maven Central. Please merge this PR only after a verifier release that has both #517 and #525. If #525 is not merged, drop the declarationPositions lines from the two DTOs (one line each) and use declarationPosition in renderLocation again. The gloss part only needs #517.

I tested it locally against #525's head (9d1bb1e, which contains main), installed as 0.0.38 in an isolated Maven repository.

Before → after (Locations section, at the study width)

Before is main, with its server built on verifier main. After is this PR on #525's head. Headless VS Code, 1600×900, Dark Modern, default side bar.

A1_01: both froms, each with its gloss

  E_OSS_A1_01_SlideRecoder.java:136
  ImageWriteParamRefinements.java:110
+ ImageWriteParamRefinements.java:111
+ where compressionExplicit(this) means compression(this) == compressionExplicit
+ where compressionTypeSet(this) means compression(this) == compressionTypeSet

A1_38

  E_OSS_A1_38_FormatReaderManager.java:157
  BufferedInputStreamRefinements.java:81
+ where marked(this) means markState(this) == marked, open(this) means stream(this) == open

A1_56: + where redoable(this) means redoState(this) == redoable
A1_09: + where notDisplayable(this) means display(this) == notDisplayable
A2_04: unchanged. @Refinement("_ >= 0") has no gloss. The missing Hint in the after shot comes from #525, not from this PR.

A1_01	A1_38

A1_56	A1_09

A2_04

The A1_01 and A1_09 shots are scrolled to Locations. The yellow outline is the focus left on Hints by the screenshot script.

Overlap with open PRs

• Show the Context tab's refinements as the error messages show them #186 (Context tab) may conflict in client/src/webview/views/sections.ts. It changes renderVariableHighlightButton and the imports, right after renderLocation, which this PR edits.
• List Found as facts and show only readable simplification steps #185 (Found as facts) may conflict in client/src/types/diagnostics.ts. Both PRs add fields to RefinementError and StateRefinementError, in nearby hunks. No conflict in logic.
• Wrap the Verification panel at spaces and operators, one conjunct per line #189 (panel wrapping): the notes are in the Locations <pre>, which keeps break-word, so a long compressionExplicit(this) can still wrap inside the name at 240 px (see A1_01). They do not share files apart from styles.ts, in separate rules.

Checks

npm run test:unit (125 passed; the new test fails on main and also checks the copied text), npm run test:typecheck, npm run lint, server mvn -B test (39 passed, against #525 as 0.0.38; the converter test now also checks the notes and the positions).

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

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

Fixed

• renderLocation reads the positions and the notes from one narrowed declaration, instead of two separate type checks.
• The notes are shown only when a declaration link is shown, so a note never appears without its link.

Declined

• DRY: declarationPositions and declarationNotes are declared on both RefinementErrorDTO and StateRefinementErrorDTO. This follows the existing declarationPosition. Moving them into LJErrorDTO would add them to every error type, most of which have no declaration.
• declarationNotes ?? [] is kept as a guard, because lsp4j leaves out null fields.

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main:

• [P1] Use a published verifier version (server/pom.xml). liquidjava-verifier:0.0.38 is not on Maven Central yet, so the server build fails.
• [P2] Format declaration positions when copying diagnostics (diagnostics.ts). The copy button would paste the new declarationPositions as raw JSON.

Fixed

• P2: formatDiagnosticForClipboard now skips declarationPositions, as it already skips declarationPosition. The copied text keeps Declaration Notes: where …. The location test now also checks the copied text.

Declined

• P1: this is intended and stated in the PR body. The PR needs the 0.0.38 release with Show states of named sets by their set in state hints and declared-here liquidjava#517 and #525, and should not be merged before that release. I tested it locally against #525's head, installed as 0.0.38 in an isolated Maven repository.

Tests: 125 unit, typecheck, lint, and 39 server tests (against 0.0.38 from #525) pass.

[CatarinaGamboa]

Codex review, round 2

• [P1] Publish the verifier version before depending on it (server/pom.xml). This is the same point as round 1.
• [P2] Show declaration notes when no declaration link exists (sections.ts).

Declined (both)

• P1: declined for the same reason as in round 1. The PR waits for the 0.0.38 release and says so in its body.
• P2: the notes explain the declaration excerpt. The verifier prints them only under that excerpt (LJDiagnostic.toString() prints getDeclarationNotes() only after a declaration snippet). Without a declaration link, a line such as where closed(this) means … would point at nothing the user can see. The server test builds that combination only to check that the field is copied. It is not a case the verifier produces.

Codex found nothing else, so the loop ends here.