[CatarinaGamboa]

Closes #532. Stacked on #530 (→ #528 → main). Retarget it to main before #530 is merged with --delete-branch.

Every message that shows code now marks it with backticks, inside the message string:

• headlines (found … but expected …, expected … but could not prove it);
• hints;
• origin notes;
• the declared-here gloss (where … means …);
• alias where lines;
• counterexamples.

How each client sees it

• Plain text (getMessage(), getMessageNotes(), Hint.message(), getCounterexampleStr(), getDeclarationNotes(), and so the Problems tab and the hover): the string with backticks, as rustc writes its messages.
• CLI: each span in blue (the existing Colors.BLUE), without backticks. The backticks stay when colour is off: NO_COLOR set (https://no-color.org) or no console (output piped or redirected). The colour switch applies to code spans only; the CLI's other colours are unchanged.
• IDE: the same backticked strings, plus LJDiagnostic.getReferences(), a List<SourceReference> with one entry per line reference. See below.

Escaping: Code.of fences code that holds backticks with a longer run, and pads it with one space on each side when it holds a backtick or starts or ends with a space: `` c == '`' ``. Code.render strips exactly that padding, so it shows any non-empty code exactly as marked.

Source references (for vscode-liquidjava#192)

record SourceReference(String message, String text, int start, String file, int line, int column):

• message: the whole message line it belongs to, exactly as getMessageNotes() or Hint.message() gives it;
• text: the words of message that name the place, e.g. line 134 or ArrayListRefinements.java:162;
• start: where text starts in message, as a UTF-16 index (a Java/JS string index), so message.substring(start, start + text.length()) is text. Use it instead of searching, because the code of a call can hold the same words (d.lock("line 18") on line 18);
• file: the absolute path; line, column: 1-based, from Spoon.

Who carries one:

• every origin note: the call, parameter, constructor or return-refinement declaration it names;
• the deciding-argument hint (… on line 20 decides …), through the new Hint.reference(), which is null for other hints.

getReferences() returns the notes' references first, then the hints'.

Before → after (CLI piped, so backticks shown)

A1_38  State Refinement Error: found `stream(buffered) == open && markState(buffered) == unmarked` but expected `markState(buffered) == marked && stream(buffered) == open`
         Origin: line 134, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`
         - Call `buffered.mark(int)` before this call; afterwards `markState(buffered) == marked`
         where `marked(this)` means `markState(this) == marked`, `open(this)` means `stream(this) == open`
A1_01    Origin: line 130, `writer.getDefaultWriteParam()` returns `compression(wParam) == compressionNotExplicit`
         - Call `wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT)` before this call; afterwards `compression(wParam) == compressionExplicit`
A2_04  Refinement Error: expected `timeout >= 0` but could not prove it
         Origin: line 94, `timeout` is a parameter of `checkCimReachable(String, int)` with no refinement
          --> Counterexample: `timeout == -1`
A1_56    Origin: line 69, `frame.getUndoManager()` says nothing about `redoState(undoManager)`
         - Guard this call with `if (undoManager.canRedo())`; inside it, `redoState(undoManager) == redoable`
A2_10  Refinement Error: found `failures.size() == size(this.failures) && failures.size() >= 0` but expected `failures.size() > 0`
         Origin: ArrayListRefinements.java:162, `failures.size()` guarantees only `failures.size() >= 0`

For all eight tasks (six study tasks and both practice tasks), the output with backticks removed is byte-identical to #530's. Each task still gives exactly one error, on its reportedLine. On a terminal the spans are blue and the backticks are gone. With NO_COLOR=1 the backticks stay.

Changes

• Code (of, render), SourceReference, and Colors.enabled().
• LJDiagnostic:
  • addMessageNote(SourceReference) and getReferences();
  • toString renders the message, notes, counterexample, hints and declaration notes.
• Marked at the leaves where messages are built:
  • ErrorMessage (both headline frames);
  • RefinementError (counterexample, alias lines);
  • AuxStateHandler.addMeanings (gloss);
  • StateHints: each state name, call, receiver and constructor, with the prose words or, and, then, with left unmarked;
  • OriginNotes/StateOrigin, whose notes are now SourceReferences.
• NotFoundError marks the missing name and the suggestion (Alias `Positiv` could not be found, Did you mean `Positive`?).
• Not marked: the other error kinds (state conflicts, syntax errors) and warnings, which the issue does not list. They are a follow-up if wanted.

Tests

• 59 existing expectations gained backticks. Each change was made by a script that accepts a new string only if removing its backticks gives exactly the old one.
• TestStateHints.assertHints compares kind and message.
• New tests, each failing without the change:
  • CodeTest (fence, colour on and off);
  • TestOriginNotes.noteNamesTheLineOfTheCallForClientsToLinkTo;
  • a reference check in the deciding-argument hint test.

mvn test: 740 run, 0 failures.

Conflicts

• State hints: name only the state the call leads to, and no guard when a call sequence works #524 and Use found … but expected … for refinement errors, drop the general hint, declare every from #525 are merged, and this branch sits on top of them (via Origin note: say where the wrong state of a receiver comes from #528's rebase), so it does not conflict with them. The lines of their code it changes are:
  • StateHints.java, on main: the hint templates at 116–119, 131–132, 182–184, 234, 239–240, 249, 252, 258, 260, 269, 295–297, 301, 303–305, 349, and stateName at 387–389;
  • RefinementError.java, on main: 71 (counterexample) and 123 (alias where lines);
  • ErrorMessage.java 39–41 (headline);
  • AuxStateHandler.java 865–866 (gloss).
• With the Fold a state error's Found under the constants its path conditions state #529 agent's work: both may touch VCChecker.throwStateRefinementError. This PR changes only the notes' parameter type there.

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

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

Fixed:

• [core-dry] Code.of(receiver) was repeated about ten times in StateHints. It is now one field, shownReceiver; only the static decidingArgument marks it inline.
• [solid-srp] Marking (Code.of) and rendering (Code.render) sit in one small class. Producers only mark, and only LJDiagnostic.toString renders, so no producer knows about ANSI.
• [testability] Code.render(message, colour) takes the colour flag as a package-visible overload, so CodeTest covers colour on and off without depending on the console.

Declined:

• [solid-ocp] Structured segments instead of backticks. The PM chose backticks in the string (rustc style), which keeps plain-text clients working unchanged.
• [core-dry] SourceReference.message repeats the note text. It is what ties a reference to its line for a client, and each reference carries exactly one line, so I kept it rather than index into getMessageNotes() (where RefinementError puts alias lines first).
• [func-few-arguments] SourceReference has 5 components. They are the minimum a client needs to find the words and open the place.

[CatarinaGamboa]

Codex review, round 1

codex exec review:

[P2] Preserve whitespace inside code spans. Code.render(Code.of(" x "), true) shows x: the trim can't tell Code.of's padding from the code's own spaces.

Soundness prompt. It found three issues:

1. Unmarked code in not-found errors: Alias 'Positiv' could not be found, Did you mean 'Positive'?.
2. Code.render edge cases:
   • " a " loses its spaces;
   • multi-line code and empty code stay fenced;
   • two spans written back to back ( `ab` ``) are read as one;
   • backticked prose outside Code.of is coloured.
3. A reference's words occurring twice: Origin: line 18, d.lock("line 18") makes ….

Fixed in "Keep the spaces of code, name where a reference starts, mark names not found":

• render strips the padding only when Code.of added it, that is when the inner code starts or ends with a backtick. " a " keeps its spaces. Spans now match across line breaks.
• SourceReference gains start, the index of text in message. The deciding-argument hint computes it from how the message is built, so a call whose code holds line 20 cannot mislead a client. Origin notes start their reference right after Origin: .
• NotFoundError marks the missing name and the suggestion.
• Tests: CodeTest covers spaces and line breaks, and both reference checks assert start.

Declined:

• Empty code. No message builds an empty code span.
• Two spans back to back, and backticks in prose. Code.of never puts two spans side by side without words between them, and none of the verifier's message text has backticks of its own.

The study tasks are byte-identical to the previous commit. Tests: 740 run, 0 failures.

[CatarinaGamboa]

Codex review, round 2

codex exec review: "I found no actionable regressions in the changed code."

Soundness prompt. It found no verifier program with code left unmarked, prose marked, or a wrong reference. It reported three direct Code strings:

1. **" ":** Code.ofgave ``` `` `` ```, and render dropped the code's own spaces. The padding rule was ambiguous for code that starts and ends with a space and also holds a backtick.
2. Code.of("a") + Code.of("b"): two spans with nothing between them read as one.
3. Code.of(""): empty code stays fenced.

Fixed (1) in "Pad code that holds a backtick or ends with a space, so render keeps it exact". Code.of pads with one space on each side whenever the code holds a backtick or starts or ends with a space, and render strips exactly one space on each side when both are there. The round trip is now exact for every non-empty code; " ", " x "and" x "are checked, andCodeTestcovers" ".

Declined (2) and (3). No message builds an empty span or puts two spans side by side without words between them: every template separates its spans with prose or , . Supporting them would need a real lexer for a case that cannot occur.

The study tasks are byte-identical. Tests: 740 run, 0 failures.

[CatarinaGamboa]

Codex review, round 3

codex exec review: "I found no actionable regressions in the diff."

Soundness prompt: it found no Code.render mismatch and no wrong SourceReference. It found unmarked code in three spec-declaration diagnostics built in TypeChecker:

• State set name 'Door' must be an identifier that starts with a lowercase letter;
• State 'ready' is in two state sets of DuplicateState: phase and access;
• State set name 'undo' is also the name of a method of SetMethodCollision, so undo(x) == ready reads like a call to undo()… (warning).

Declined for this PR, as a follow-up. #532 lists headlines, hints, origin notes, the gloss and counterexamples, the messages a participant reads when a call or value is wrong. These three report mistakes in the specification itself. They go through CustomError/CustomWarning, whose text LJDiagnostic.toString already renders, so marking them later is a change to their strings only. I'll list them, with the other error kinds (state conflicts, syntax), as a follow-up for the PM.

This ends the Codex loop for this PR: nothing relevant to #532's scope is left.