Show the code of messages in the editor font and link the lines they name by CatarinaGamboa · Pull Request #193 · liquid-java/vscode-liquidjava

CatarinaGamboa · 2026-11-10T23:23:05Z

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 · 2026-11-10T23:23:57Z

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 · 2026-11-10T23:25:52Z

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.

…194) Fixes the integration failure on main after #191 (stable) and the earlier ones on #189 (minimum) and #193 (both). Each time it was the same test timing out: `smoke.test.ts` › "activates, becomes ready, and verifies its isolated fixture". ## Cause The server only verifies when the first file of the workspace is opened (`LJDiagnosticsService.didOpen`). In the `failing` fixture, `state-errors.test.ts` runs first and opens and verifies the fixture. The smoke test then opens `FailingRefinement.java` and waits for a verification that the server never starts. It passed only when a late notification from the earlier test happened to arrive while it waited, which is why it failed on some runs and VS Code versions and not others. ## Change The smoke test waits for the verification on open only when the fixture has not been verified yet. It still runs the manual `liquidjava.verify` and checks its result as before. ## Tests - With a 5 s pause at the start of the smoke test, so every earlier notification has arrived: main times out exactly as in CI; this branch passes. - Without the pause: `xvfb-run -a npm test` (VS Code 1.82, the minimum) passes twice in a row, 9 + 1 tests; `test:typecheck` and `lint` pass. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…name The server sends each diagnostic's message notes and the source references of its notes and hints. The panel shows the notes under Found, and renders every message line (headline, notes, hints, declared-here gloss) with the code the verifier marks in backticks in the editor font and each reference, such as `line 134`, as a link that opens that line. Needs a liquidjava-verifier release with liquid-java/liquidjava#528, #530 and #533. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…an error alike (#196) Closes #175 Verifier 0.0.38 (liquid-java/liquidjava#493, already the dependency on main) names variables as in code and, only when an error has several values of one name, tags the others with the line their value comes from: `preview@51`. The message and the Context tab already used those names. The rest of the panel did not: the server formatted the Expected, the Found steps, the counterexample and the translation table with the verifier's default formatter. That formatter numbers clashes within each expression, so the Found of A3_07 showed three different values of `preview` all as `∀preview`, and `preview#1` meant a different value on each line. ## What 0.0.38 sends - **Tag format:** `x@51`. When tagged values share a line, `x@25#1`, `x@25#2`; with no line, `x#2`. A call argument can carry one too: `failures.size()@84`. No Unicode superscripts any more. - **Where:** the message, the counterexample in the message, the message notes and hints, and the Context tab (`ContextDisplay`, merged in #186) already use the names. `LJError.getDisplayNames()` gives the error's names for refinement and state refinement errors; nothing else is pre-formatted for the IDE. ## What changes **Server** (`server/src/main/java/dtos`) - `RefinementErrorDTO` and `StateRefinementErrorDTO` format the expected, each step's binder and predicate (`VCImplicationDTO`), and the counterexample with `error.getDisplayNames()`. - `TranslationTableDTO` keys each entry by the error's name for it (`preview@51`), so a tagged binder still opens its source. Errors without names keep the plain key. **Webview** - A tag is drawn as a subscript: `preview` with a small `l51` below, titled "value of preview at line 51" (`x@25#2` → `l25#2`, "value 2 of x at line 25"). This applies in every highlighted expression (Expected, Found, steps, counterexample, Context), in the binders, and in the code of messages, notes and hints. Copy, the hover and the Problems panel keep the ASCII `preview@51`. - The step diff keeps `preview@51` as one token, so a changed tag highlights its whole variable. - String and character literals are kept whole when highlighting and diffing, so `"a@1"` is not read as a tag. - The regexes no longer match `⁰-⁹`. - The Context tab's Name column renders a variable without a source position the same way as one with a position (before, it was raw text). - Rows the error mentions are still marked in the Context tab: the translation-table keys are compared without their tag, as before. ## Against the issue's to-do - Render the tag: done (subscript + tooltip). **Click-to-source:** works on binders (`∀preview@51`) through the re-keyed translation table. A tag inside a predicate shows only the tooltip, because the highlighter has no translation table. The line number is in the tag itself. - Tokenize as one identifier: done (step diff and highlighter). The Unicode superscript handling is gone. - **Context view: already done** by #186 (`ContextDisplay` with `DisplayNames` and `ContextHistory.lineOf`). This PR only renders its tags the same way. - Translation table keyed by display name: done. - **Bump the verifier: already done**, main depends on 0.0.38. ## Screenshots (headless VS Code, light theme, verifier 0.0.38) **A3_07 ScannerOutputStage**, the study exercise with several values of `preview`. | | before (main) | after | |---|---|---| | Found, a step back (9/10) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-before-step.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-after-step.png) | | Found, original (1/10) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-before-original.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-after-original.png) | | Context tab | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-before-context.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-after-context.png) | **A2_08 LogWindow**, plain names (no change, as for every other study exercise): | before (main) | after | |---|---| | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A2_08-before.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A2_08-after.png) | ## Not in this PR - Explaining generated names such as `#if_condition` (#195). - **Different scopes.** The Context tab names variables per context (declared variable plain) and the error per error (latest shown value plain). The same value can be `preview@54` in the Context tab and `preview` in the error, as in the A3_07 screenshots. Making them agree would mean a verifier change. ## Expected conflicts - #185 (`study-found-box`): merges cleanly with its current head. It changes `vc-implications.ts` and `styles.ts`; this PR adds one rule to `styles.ts` and changes `TOKEN_PATTERN` and `renderBinder` in `vc-changes.ts`. Any conflict would be in `styles.ts` (adjacent rules). - #193 is merged; this PR changes one line of `message-text.ts`. ## Tests - Server `DiagnosticConverterTest`: verifies a `b = -b` fixture and checks that the message, every Found step (`∀b@6 b@6 == 8`, `∀b@7 b@7 == b@6 && b@7 > 0`, `∀b b == -b@7`), the expected, the counterexample and the translation-table keys use the same names. On main the steps read `∀b b == b#1 && b > 0`. - Client `vc-changes.spec`: tags render as subscripts with their tooltip (also after a call and with a number). A changed tag is diffed with its variable. A literal is left alone. `diagnostics.spec`: a tag in a message's code, next to a literal. `context.spec` was updated to the rendered tag. - Local: `npm run test:unit` (134), `test:typecheck`, `lint`, `mvn -B package` (44), `VSCODE_TEST_VERSION=minimum xvfb-run -a npm test` (9 + 1 passing). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

… as markdown, and code in the view as in the hover (#198) 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 | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-hover-before-dark.png" width="430"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-hover-card-dark.png" width="430"> | | Hover, light | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-hover-before-light.png" width="430"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-hover-card-light.png" width="430"> | | Problems tab, dark | (headline + notes + counterexample as plain text) | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-problems-card-dark.png" width="430"> | | View, dark | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-panel-before-dark.png" width="300"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-panel-after-dark.png" width="300"> | | View, light | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-panel-before-light.png" width="300"> | <img src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-panel-after-light.png" width="300"> | 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; #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 #196); the conflict in `webview/message-text.ts` resolved as described in the overlap note of the first version. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…r lines (#199) Closes #195 Names the verifier gives values of the code, such as `#if_condition`, `#getUndoManager_result` or `#case_condition@74`, now explain themselves on hover in plain words. When their source line is known, the hover gives it and a click goes there. ## What the verifier already sends **No verifier change is needed.** Since 0.0.38 (#196), the error's translation table is keyed by the name as shown, and it holds a position for every generated name in the error: - `#if_condition` → the condition, `#getUndoManager_result` → the call, `#case_condition@74` → its `case`, and so on. - Several values of one kind get distinct names (`#case_condition@71` … `@74`), so they no longer share one entry. The issue's note about this is out of date. - In A1_56, all 11 generated names in the 19 steps are in the table. The Context tab has no translation table. There, the server leaves out generated variables. This PR adds one field, `generatedPlaces` (name as shown → place). The server code is in this repo, so this is still a vscode-only change. ## What the hover says The text is the title of the name, with "at line N" when the line is known and "Click to go to it." when the name is a link. Every title ends with "LiquidJava gives it the name #…". | Name | Hover | |---|---| | `#if_condition` | The condition of the if at line N | | `#loop_condition` | The condition of the loop at line N | | `#ternary_condition` | The condition of the ? : at line N | | `#switch_selector` | The value the switch at line N checks | | `#case_condition` | Whether the case at line N matches | | `#try_branch` | Whether the try block at line N runs to its end, rather than a catch block | | `#catch_branch` | Whether this catch block of the try at line N runs, rather than a later one | | `#array_length` | The length of the array created at line N | | `#new_File` | The new File object created at line N | | `#size_result` | The value returned by the call to size() at line N | | `#count_value` | The value of the field count read at line N | | `#operation_result` | The result of the operation at line N | | `#expression_value` | The value of the expression at line N | **Where the line comes from:** - First, the error's translation table (the Context tab uses `generatedPlaces`). The name is then a link. - Otherwise, the name's line tag (`@74`). The line is shown, but the name is not a link. - Otherwise, the line is left out. **`extended#1`** is not a generated name. It is a line tag with no line, on a program variable, and #196 already explains it ("the 1st value of extended (line unknown)"). ## Where - **Expected.** - **Found steps:** - the binder column: the title of `∀#if_condition` was "Go to source (boolean)"; it is now the explanation, and the click still highlights the source; - the predicates. - **The step diff:** both the changed fragments and the unchanged tokens. - **The counterexample.** - **The Context tab's refinements.** The names have a dotted underline, like the binders, and a pointer cursor when they are links. A link uses the same `location-link` click as the message references from #193. ## Screenshots A1_56 EditCommand, Found at step 7/20, in headless VS Code (openvscode-server) with verifier 0.0.38. **Headless screenshots do not capture native tooltips.** The box under the name is drawn by the screenshot script from the element's real `title` attribute. On main, the same box shows "(no tooltip)" for the predicate and "Go to source (boolean)" for the binder. | | before (main) | after | |---|---|---| | `#getUndoManager_result` in a predicate, dark | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-predicate-before-dark.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-predicate-after-dark.png) | | `∀#if_condition` binder, dark | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-binder-before-dark.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-binder-after-dark.png) | | `#getUndoManager_result`, light | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-predicate-before-light.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-predicate-after-light.png) | | `∀#if_condition` binder, light | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-binder-before-light.png) | ![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-binder-after-light.png) | There is no Context tab screenshot. In A1_56, the Context tab replaces each generated value by its expression or drops it, so no generated name is left to show. The unit test covers the Context tab. ## Changes - `client/src/webview/generated-names.ts` (new): the kinds and their wording, the hover text, and the rendered name. - `highlighting.ts`: the highlighter takes an optional `places` table (name → place). A generated name, together with its line tag, is rendered by `renderGeneratedName`. - `vc-changes.ts`, `errors.ts`, `counterexample.ts`, `context/*.ts`: pass the table through. `renderBinder` uses the explanation as its title. - Server: `ContextHistoryDTO.generatedPlaces`, filled by `ContextHistoryConverter`. ## Tests - `vc-changes.spec`: one test, which fails on main. It checks: - a binder linked through the table; - a predicate name that is linked, one with no place, and one with only a tag line; - `#ret`, which is left alone; - a binder with only a tag; - the diff path. - `context.spec`: one test, which fails on main: a refinement's name linked through `generatedPlaces`. - `ContextHistoryConverterTest`: `#array_length` of the Door fixture has its place. - Local runs: - `npm run test:unit` (142), `test:typecheck`, `lint`; - `mvn -B package` (45); - `VSCODE_TEST_VERSION=minimum xvfb-run -a npm test` (9 + 1 passing). ## Not in this PR - The headline message (`found … #getUndoManager_result …`) and the editor hover are markdown or plain text with no translation table, so their names are not explained. - `#ret` (a method's return value) is not one of the verifier's generated kinds and is left as is. - A method named `operation` or a field named `expression` would be described as an operation result or expression value, because the verifier names them alike. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa added a commit that referenced this pull request Nov 10, 2026

Screenshots for #193

b85786f

CatarinaGamboa force-pushed the feat/181-declaration-notes branch from d0a4a6e to 43580f4 Compare November 11, 2026 14:28

CatarinaGamboa force-pushed the feat/192-code-spans branch from fe43a0e to 950ac38 Compare November 11, 2026 14:28

CatarinaGamboa changed the base branch from feat/181-declaration-notes to main November 11, 2026 16:52

CatarinaGamboa mentioned this pull request Nov 11, 2026

Smoke test: do not wait for a verification the server does not start #194

Merged

CatarinaGamboa force-pushed the feat/192-code-spans branch from f482149 to d72cf4d Compare November 11, 2026 17:07

CatarinaGamboa and others added 2 commits November 11, 2026 17:09

Test that the server sends the message notes and their references

04c6859

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

CatarinaGamboa force-pushed the feat/192-code-spans branch from d72cf4d to 04c6859 Compare November 11, 2026 17:11

CatarinaGamboa merged commit d73c500 into main Nov 11, 2026
3 checks passed

CatarinaGamboa mentioned this pull request Nov 11, 2026

Explain the verifier's generated names on hover and link them to their lines #199

Merged

Navigation Menu

Repository navigation

Show the code of messages in the editor font and link the lines they name - #193

Show the code of messages in the editor font and link the lines they name#193
CatarinaGamboa merged 2 commits into
mainfrom
feat/192-code-spans

CatarinaGamboa commented Nov 10, 2026 •

edited

Loading

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

CatarinaGamboa commented Nov 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What changes

Verifier version

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

Hover: the two options

Overlap with open PRs

Checks

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Clean-code review

Uh oh!

CatarinaGamboa commented Nov 10, 2026

Codex review, round 1

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

CatarinaGamboa commented Nov 10, 2026 •

edited

Loading