[CatarinaGamboa]

Closes #188

What changes

The editor diagnostic that LJDiagnosticsHandler publishes now carries:

1. the headline (<title>: <message>), as before;
2. then each of the verifier's message notes, LJDiagnostic.getMessageNotes(), one per line;
3. then the verifier's counterexample, getCounterexampleStr(), when it has one.

That text is what the hover and the Problems view show. Hints are left out, since they stay collapsed in the panel by design.

The server reads the verifier's generic LJDiagnostic API, not a per-error list. So any note the verifier adds later appears in the hover with no extension change. That includes the planned From note (liquid-java/liquidjava#522), and a counterexample for state errors once the verifier gives one.

Before → after (hover text, verifier 0.0.37)

A2_04

  Refinement Error: expected timeout >= 0 but could not prove it
+ Counterexample: timeout == -1

A2_10

  Refinement Error: failures.size() == size(this.failures) && failures.size() >= 0 is not a subtype of failures.size() > 0
+ Counterexample: failures.size() == 0

A1_38, A1_01, A1_56 and A1_09 are unchanged. Their errors have no message notes and no counterexample in 0.0.37 or main.

	Before	After
A2_04
A2_10

(Headless VS Code, 1600×900, Dark Modern.)

Verifier version

0.0.37, already released. getMessageNotes() and getCounterexampleStr() are both in it, and the branch builds with the current pom. Today the only message notes are the where <alias> means … lines of refinement errors that use aliases, and no study task has one. The From note will come with a later verifier release.

Open question for the PM

The issue lists the where … means … gloss among the notes. In the verifier, the gloss is a declaration note (getDeclarationNotes(), liquid-java/liquidjava#517, needs 0.0.38). It explains the "declared here" excerpt, which the hover does not show. So this PR shows only the message notes, as specified. If the hover should also show the gloss, that is one more lines.addAll(diagnostic.getDeclarationNotes()), but it needs the 0.0.38 bump that #191 makes.

Overlap with open PRs

Server only, in LJDiagnosticsHandler. No conflict with #185, #186, #189 or #191.

Checks

Server mvn -B test (40 passed; new LJDiagnosticsHandlerTest, which fails on main), npm run test:unit (124 passed), npm run test:typecheck, npm run lint.

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

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

Already in the diff

• Building the message is a small static getHoverMessage, out of the groupingBy lambda, so it can be tested on its own (SRP).

Declined

• Renaming getHoverMessage to a broader name (the Problems view shows the same text). The issue and the reviewers talk about the hover, so the name says why the lines are there.

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main: no findings. Its summary: "The change adds diagnostic notes and counterexamples to editor messages without changing the existing headline. The server tests pass."

The loop ends here: nothing to fix.