From c353a66dddcaac3d2a14cf6368d0668d47d29c83 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 23:22:29 +0000 Subject: [PATCH 1/2] Show the code of messages in the editor font and link the lines they 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 --- client/src/types/diagnostics.ts | 13 ++++++ client/src/webview/message-text.ts | 45 +++++++++++++++++++ client/src/webview/script.spec.ts | 4 +- client/src/webview/state-errors.spec.ts | 2 +- client/src/webview/styles.ts | 11 +++++ .../views/diagnostics/diagnostics.spec.ts | 20 ++++++++- .../src/webview/views/diagnostics/errors.ts | 7 +-- .../src/webview/views/diagnostics/warnings.ts | 7 +-- client/src/webview/views/sections.ts | 27 +++++++---- .../dtos/diagnostics/LJDiagnosticDTO.java | 14 +++++- .../dtos/diagnostics/SourceReferenceDTO.java | 26 +++++++++++ 11 files changed, 156 insertions(+), 20 deletions(-) create mode 100644 client/src/webview/message-text.ts create mode 100644 server/src/main/java/dtos/diagnostics/SourceReferenceDTO.java diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 4bb81ce..a65aa59 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -32,12 +32,25 @@ export type LJHint = { message: string; }; +// a place in the source that a line of a diagnostic, a message note or a hint, names, such as `line 134` +export type LJSourceReference = { + message: string; + text: string; + // where text starts in message + start: number; + position: SourcePosition; +}; + type BaseDiagnostic = { title: string; message: string; hints: LJHint[]; file: string; position: SourcePosition | null; + // lines under the message that explain it, such as where a value comes from + messageNotes: string[]; + // the places the message notes and the hints name + references: LJSourceReference[]; } export type CustomError = BaseDiagnostic & { diff --git a/client/src/webview/message-text.ts b/client/src/webview/message-text.ts new file mode 100644 index 0000000..f45b2cb --- /dev/null +++ b/client/src/webview/message-text.ts @@ -0,0 +1,45 @@ +import type { LJSourceReference } from "../types/diagnostics"; +import { escapeHtml } from "./utils"; + +// a run of backticks, the code, and a run of the same length, as the verifier marks code in its messages +const CODE_SPAN = /(`+)([\s\S]+?)(? + reference.message === message && message.startsWith(reference.text, reference.start)); + let html = ""; + let index = 0; + while (index < message.length) { + const link = links.find(reference => reference.start === index); + if (link) { + html += renderReferenceLink(link); + index += link.text.length; + continue; + } + CODE_SPAN.lastIndex = index; + const span = message[index] === "`" ? CODE_SPAN.exec(message) : null; + if (span) { + html += `${escapeHtml(unpad(span[2]))}`; + index += span[0].length; + continue; + } + html += escapeHtml(message[index]); + index++; + } + return html; +} + +// the code without the space on each side that the verifier adds to code that holds a backtick or a space at an end +function unpad(code: string): string { + return code.length >= 2 && code.startsWith(" ") && code.endsWith(" ") ? code.slice(1, -1) : code; +} + +function renderReferenceLink(reference: LJSourceReference): string { + const { position } = reference; + return /*html*/`${escapeHtml(reference.text)}`; +} diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index 70ac935..64563af 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -18,7 +18,7 @@ function diagnostic(file: string, title: string, category: 'error' | 'warning' = const details = { title, message: `${title} message`, - hints: [], + hints: [], messageNotes: [], references: [], file, position: { ...position, file }, }; @@ -60,7 +60,7 @@ const stateMachine: LJStateMachine = { function stateError(title: string, sm: LJStateMachine, line = position.lineStart, file = currentFile): LJDiagnostic { const errorPosition = { ...position, file, lineStart: line, lineEnd: line }; return { - title, message: `${title} message`, hints: [], file, position: errorPosition, + title, message: `${title} message`, hints: [], messageNotes: [], references: [], file, position: errorPosition, category: 'error', type: 'state-refinement-error', translationTable: {}, expected: 'Open(counter)', found: { implication: null as never, origin: null, simplification: 'Closed(counter)' }, customMessage: '', declarationPosition: null, declarationPositions: [], declarationNotes: [], stateMachines: [sm], diff --git a/client/src/webview/state-errors.spec.ts b/client/src/webview/state-errors.spec.ts index 51f1f50..07c39ec 100644 --- a/client/src/webview/state-errors.spec.ts +++ b/client/src/webview/state-errors.spec.ts @@ -20,7 +20,7 @@ function stateError(line: number, overrides: Partial = {}) const file = overrides.file ?? callerFile; return { category: 'error', type: 'state-refinement-error', title: 'State Refinement Error', - message: 'found childrenAllowed(root¹⁸) but expected maybeHasChildren(root¹⁸)', hints: [], + message: 'found childrenAllowed(root¹⁸) but expected maybeHasChildren(root¹⁸)', hints: [], messageNotes: [], references: [], file, position: { file, lineStart: line, colStart: 15, lineEnd: line, colEnd: 35 }, translationTable: {}, expected: 'maybeHasChildren(root¹⁸)', found: { implication: null as never, origin: null, simplification: null }, diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index c3f0d68..90651db 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -232,8 +232,19 @@ export function getStyles(): string { padding: 0.5rem; background-color: var(--vscode-editor-background); border-radius: 4px; + } + /* code that a message marks with backticks, set apart from its prose */ + .lj-code { + padding: 0 0.2em; + border-radius: 3px; font-family: var(--vscode-editor-font-family, monospace); font-size: var(--vscode-editor-font-size, inherit); + color: var(--vscode-textPreformat-foreground); + background-color: var(--vscode-textPreformat-background); + overflow-wrap: break-word; + } + .message-note { + margin: 0 0 0.25rem; } .hint-message { white-space: pre-wrap; diff --git a/client/src/webview/views/diagnostics/diagnostics.spec.ts b/client/src/webview/views/diagnostics/diagnostics.spec.ts index c2bcb7a..2b17bcc 100644 --- a/client/src/webview/views/diagnostics/diagnostics.spec.ts +++ b/client/src/webview/views/diagnostics/diagnostics.spec.ts @@ -9,14 +9,14 @@ const otherFile = 'file:///workspace/Other.java'; function error(file = currentFile, title = 'Invalid refinement'): CustomError { return { category: 'error', type: 'custom-error', title, - message: 'The refinement does not hold.', hints: [], file, position: null, + message: 'The refinement does not hold.', hints: [], messageNotes: [], references: [], file, position: null, }; } function warning(file = currentFile): CustomWarning { return { category: 'warning', type: 'custom-warning', title: 'Verification warning', - message: 'Some code could not be verified.', hints: [], file, position: null, + message: 'Some code could not be verified.', hints: [], messageNotes: [], references: [], file, position: null, }; } @@ -87,6 +87,22 @@ describe('diagnostics view', () => { expect(document.querySelector('#show-all-button')).toBeNull(); }); + it('shows the code of notes and hints in the editor font, and links the lines they name', () => { + const note = 'Origin: line 134, `new BufferedInputStream(stream)` makes `markState(b) == unmarked`'; + const position = { file: '/workspace/Reader.java', lineStart: 133, colStart: 8, lineEnd: 133, colEnd: 8 }; + document.body.innerHTML = renderDiagnosticsView([{ + ...error(), messageNotes: [note], references: [{ message: note, text: 'line 134', start: 8, position }], + hints: [{ kind: 'general', message: "Call `` b.f('`') `` first" }], + }], false, currentFile); + + const link = document.querySelector('.message-note a.location-link'); + expect(link?.textContent).toBe('line 134'); + expect([link?.getAttribute('data-file'), link?.getAttribute('data-line')]).toEqual(['/workspace/Reader.java', '133']); + expect(text('.message-note')).toBe('Origin: line 134, new BufferedInputStream(stream) makes markState(b) == unmarked'); + expect(Array.from(document.querySelectorAll('.lj-code')).map(code => code.textContent)) + .toEqual(['new BufferedInputStream(stream)', 'markState(b) == unmarked', "b.f('`')"]); + }); + it('shows every declaration of a refinement with their notes under them', () => { const declaredAt = (lineStart: number) => ({ file: '/workspace/DoorRefinements.java', lineStart, colStart: 29, lineEnd: lineStart, colEnd: 58 }); diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index 0e58ed4..bc7861f 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -1,4 +1,4 @@ -import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton, renderHints } from "../sections"; +import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton, renderHints, renderMessageNotes } from "../sections"; import { renderCounterexample } from "./counterexample"; import { renderVCImplication } from "./vc-implications"; import type { @@ -76,9 +76,10 @@ export function renderError(error: LJError, actions = ''): string { const message = error.type === 'refinement-error' || error.type === 'state-refinement-error' ? error.customMessage : error.message; const header = renderDiagnosticHeader(error.title, message || '', actions); const content = (errorContentRenderers[error.type] as (error: LJError) => string)?.(error) || ''; - const hint = renderHints(error.hints, getDiagnosticKey(error)); + const notes = renderMessageNotes(error); + const hint = renderHints(error.hints, getDiagnosticKey(error), error.references); const location = renderLocation(error); - return /*html*/`${header}${content}${hint}${location}`; + return /*html*/`${header}${content}${notes}${hint}${location}`; } function renderDiagnosticContextAction(error: LJError): string { diff --git a/client/src/webview/views/diagnostics/warnings.ts b/client/src/webview/views/diagnostics/warnings.ts index e718bc5..9c46d49 100644 --- a/client/src/webview/views/diagnostics/warnings.ts +++ b/client/src/webview/views/diagnostics/warnings.ts @@ -1,5 +1,5 @@ import type { CustomWarning, ExternalClassNotFoundWarning, ExternalMethodNotFoundWarning, LJWarning, UnsatisfiableRefinementWarning } from "../../../types/diagnostics"; -import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderHints, renderLocation } from "../sections"; +import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderHints, renderLocation, renderMessageNotes } from "../sections"; import { renderCopyDiagnosticButton } from "./diagnostics"; import { getDiagnosticKey } from "../../diagnostic-reveal"; @@ -34,7 +34,8 @@ const warningContentRenderers: WarningContentRenderers = { export function renderWarning(warning: LJWarning, actions = ''): string { const header = renderDiagnosticHeader(warning.title, warning.message, actions); const content = (warningContentRenderers[warning.type] as (warning: LJWarning) => string)?.(warning) || ''; - const hint = renderHints(warning.hints, getDiagnosticKey(warning)); + const notes = renderMessageNotes(warning); + const hint = renderHints(warning.hints, getDiagnosticKey(warning), warning.references); const location = renderLocation(warning); - return /*html*/`${header}${content}${hint}${location}`; + return /*html*/`${header}${content}${notes}${hint}${location}`; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 7f2a986..86189da 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -1,8 +1,9 @@ -import type { LJDiagnostic, LJHint, SourcePosition } from "../../types/diagnostics"; +import type { LJDiagnostic, LJHint, LJSourceReference, SourcePosition } from "../../types/diagnostics"; import { escapeHtml, getFileName, getSimpleName } from "../utils"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../highlighting"; import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal"; import { renderCodicon, renderCodiconButton } from "../icons"; +import { renderMessageText } from "../message-text"; import { LJVariable } from "../../types/context"; export const renderMainHeader = (title: string, selectedTab: NavTab, badges = NO_NAV_BADGES): string => /*html*/` @@ -34,8 +35,9 @@ export function setHintOpen(key: string, open: boolean) { * Several call sequences are alternatives, so they are listed as options apart from the hints that explain the error * @param hints The hints of the diagnostic * @param key Identifies the diagnostic, so opened hints stay open after a new verification + * @param references The places in the source the hints name */ -export function renderHints(hints: LJHint[] | undefined, key?: string): string { +export function renderHints(hints: LJHint[] | undefined, key?: string, references: LJSourceReference[] = []): string { const shown = (hints ?? []).filter(hint => hint.message.trim()); if (shown.length === 0) return ''; const options = shown.filter(hint => hint.kind === 'call-sequence'); @@ -49,17 +51,26 @@ export function renderHints(hints: LJHint[] | undefined, key?: string): string { ${listsOptions ? /*html*/`

Any one of these:

-
    ${options.map(hint => `
  • ${renderHintMessage(hint)}
    • `).join('')}
+
    ${options.map(hint => `
  • ${renderHintMessage(hint, references)}
    • `).join('')}
` : ''} - ${notes.map(hint => `
${renderHintMessage(hint)}
`).join('')} + ${notes.map(hint => `
${renderHintMessage(hint, references)}
`).join('')} `; } -function renderHintMessage(hint: LJHint): string { - return `${escapeHtml(hint.message.trim())}`; +function renderHintMessage(hint: LJHint, references: LJSourceReference[]): string { + return `${renderMessageText(hint.message, references)}`; +} + +/** + * Renders the notes under the message of a diagnostic, such as where a value comes from, with their links + */ +export function renderMessageNotes(diagnostic: LJDiagnostic): string { + if (diagnostic.messageNotes.length === 0) return ''; + return /*html*/`
${diagnostic.messageNotes + .map(note => `

${renderMessageText(note, diagnostic.references)}

`).join('')}
`; } export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/` @@ -74,7 +85,7 @@ export const renderDiagnosticHeader = (title: string, message: string, actions =

${title}

${actions.trim() ? `
${actions}
` : ''} -

${message}

+

${renderMessageText(message)}

`; export function renderDiagnosticDataAttributes(diagnostic: LJDiagnostic): string { @@ -97,7 +108,7 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => { const links = positions.map(renderLocationLink).join("\n"); // the notes explain the declarations, so they are shown only under their links const notes = declarationPositions.length > 0 ? declaration?.declarationNotes ?? [] : []; - const noteLines = notes.map(note => `${escapeHtml(note)}`).join(""); + const noteLines = notes.map(note => `${renderMessageText(note)}`).join(""); return renderCustomSection(title, /*html*/`
${links}${noteLines}
`); }; diff --git a/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java b/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java index d47e124..04b213b 100644 --- a/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java +++ b/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java @@ -16,14 +16,24 @@ public class LJDiagnosticDTO { public final List hints; public final String file; public final SourcePositionDTO position; + /** Lines under the message that explain it, such as where a value comes from */ + public final List messageNotes; + /** The places in the source that the message notes and hints name */ + public final List references; public LJDiagnosticDTO(String category, String type, LJDiagnostic diagnostic) { this(category, type, diagnostic.getTitle(), diagnostic.getMessage(), HintDTO.from(diagnostic.getHints()), - diagnostic.getFile(), SourcePositionDTO.from(diagnostic.getPosition())); + diagnostic.getFile(), SourcePositionDTO.from(diagnostic.getPosition()), diagnostic.getMessageNotes(), + SourceReferenceDTO.from(diagnostic.getReferences())); } public LJDiagnosticDTO(String category, String type, String title, String message, List hints, String file, SourcePositionDTO position) { + this(category, type, title, message, hints, file, position, List.of(), List.of()); + } + + private LJDiagnosticDTO(String category, String type, String title, String message, List hints, + String file, SourcePositionDTO position, List messageNotes, List references) { this.category = category; this.type = type; this.title = title; @@ -31,6 +41,8 @@ public LJDiagnosticDTO(String category, String type, String title, String messag this.hints = hints; this.file = file; this.position = position; + this.messageNotes = messageNotes; + this.references = references; } public static LJDiagnosticDTO from(LJDiagnostic diagnostic) { diff --git a/server/src/main/java/dtos/diagnostics/SourceReferenceDTO.java b/server/src/main/java/dtos/diagnostics/SourceReferenceDTO.java new file mode 100644 index 0000000..5730114 --- /dev/null +++ b/server/src/main/java/dtos/diagnostics/SourceReferenceDTO.java @@ -0,0 +1,26 @@ +package dtos.diagnostics; + +import java.util.List; + +import liquidjava.diagnostics.SourceReference; + +/** + * DTO for serializing a place in the source that a line of a diagnostic names, such as {@code line 134} + * + * @param message the whole line, a message note or a hint, as the diagnostic gives it + * @param text the words of {@code message} that name the place + * @param start where {@code text} starts in {@code message} + * @param position the place, with lines and columns from 0 as in the other positions + */ +public record SourceReferenceDTO(String message, String text, int start, SourcePositionDTO position) { + + public static SourceReferenceDTO from(SourceReference reference) { + SourcePositionDTO position = new SourcePositionDTO(reference.file(), reference.line() - 1, + reference.column() - 1, reference.line() - 1, reference.column() - 1); + return new SourceReferenceDTO(reference.message(), reference.text(), reference.start(), position); + } + + public static List from(List references) { + return references.stream().map(SourceReferenceDTO::from).toList(); + } +} From fe43a0eed50b5b85ec06a920cfb84c1237775b00 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 23:23:02 +0000 Subject: [PATCH 2/2] Test that the server sends the message notes and their references Co-Authored-By: Claude Opus 5.5 --- .../src/test/java/utils/DiagnosticConverterTest.java | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java index cc0ff4c..a0c79c2 100644 --- a/server/src/test/java/utils/DiagnosticConverterTest.java +++ b/server/src/test/java/utils/DiagnosticConverterTest.java @@ -14,8 +14,10 @@ import dtos.diagnostics.HintDTO; import dtos.diagnostics.LJDiagnosticDTO; import dtos.diagnostics.SourcePositionDTO; +import dtos.diagnostics.SourceReferenceDTO; import dtos.errors.*; import dtos.warnings.*; +import liquidjava.diagnostics.SourceReference; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.errors.*; import liquidjava.diagnostics.hints.Hint; @@ -62,6 +64,16 @@ void preservesCommonDiagnosticFields() throws Exception { assertEquals(new SourcePositionDTO(dto.file, 1, 8, 1, 18), dto.position); } + @Test + void sendsTheMessageNotesWithThePlacesTheyNameFromLineZero() { + CustomError error = new CustomError("verification failed", position); + error.addMessageNote(SourceReference.of("Origin: line 2, `value`", "line 2", 8, position)); + LJDiagnosticDTO dto = (LJDiagnosticDTO) DiagnosticConverter.convertToDTO(error); + assertEquals(List.of("Origin: line 2, `value`"), dto.messageNotes); + assertEquals(List.of(new SourceReferenceDTO("Origin: line 2, `value`", "line 2", 8, + new SourcePositionDTO(dto.file, 1, 8, 1, 8))), dto.references); + } + @Test void keepsEachHintWithItsKind() { CustomError error = new CustomError("verification failed", position);