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 <noreply@anthropic.com>

Author: CatarinaGamboa

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 & {

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]+?)(?<!`)\1(?!`)/y;
+
+/**
+ * Renders a line of a diagnostic, such as a note or a hint: the code it marks with backticks in the editor font,
+ * without the backticks, and each place in the source it names as a link that opens that place
+ * @param references the places the diagnostic names, of which only those of this line are used
+ */
+export function renderMessageText(message: string, references: LJSourceReference[] = []): string {
+    const links = references.filter(reference =>
+        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 += `<code class="lj-code">${escapeHtml(unpad(span[2]))}</code>`;
+            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*/`<a href="#" class="link location-link message-reference" data-file="${escapeHtml(position.file ?? "")}" data-line="${position.lineStart}" data-column="${position.colStart}">${escapeHtml(reference.text)}</a>`;
+}

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 },
     };
@@ -61,7 +61,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],

client/src/webview/state-errors.spec.ts

@@ -20,7 +20,7 @@ function stateError(line: number, overrides: Partial<StateRefinementError> = {})
     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 },

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;

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 });

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 { renderHighlightedLines } from "../../highlighting";
 import { renderVCImplication } from "./vc-implications";
@@ -77,9 +77,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 {

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}`;
 }

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 } 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*/`
                     <div class="hint-options">
                         <p class="hint-options-title">Any one of these:</p>
-                        <ul>${options.map(hint => `<li>${renderHintMessage(hint)}</li>`).join('')}</ul>
+                        <ul>${options.map(hint => `<li>${renderHintMessage(hint, references)}</li>`).join('')}</ul>
                     </div>
                 ` : ''}
-                ${notes.map(hint => `<div class="hint-note">${renderHintMessage(hint)}</div>`).join('')}
+                ${notes.map(hint => `<div class="hint-note">${renderHintMessage(hint, references)}</div>`).join('')}
             </div>
         </details>
     `;
 }
 
-function renderHintMessage(hint: LJHint): string {
-    return `<span class="hint-message">${escapeHtml(hint.message.trim())}</span>`;
+function renderHintMessage(hint: LJHint, references: LJSourceReference[]): string {
+    return `<span class="hint-message">${renderMessageText(hint.message, references)}</span>`;
+}
+
+/**
+ * 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*/`<div class="section message-notes">${diagnostic.messageNotes
+        .map(note => `<p class="message-note">${renderMessageText(note, diagnostic.references)}</p>`).join('')}</div>`;
 }
 
 export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/`
@@ -74,7 +85,7 @@ export const renderDiagnosticHeader = (title: string, message: string, actions =
         <h3>${title}</h3>
         ${actions.trim() ? `<div class="diagnostic-actions">${actions}</div>` : ''}
     </div>
-    <div class="diagnostic-header"><p>${message}</p></div>
+    <div class="diagnostic-header"><p>${renderMessageText(message)}</p></div>
 `;
 
 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 => `<span class="location-note">${escapeHtml(note)}</span>`).join("");
+    const noteLines = notes.map(note => `<span class="location-note">${renderMessageText(note)}</span>`).join("");
     return renderCustomSection(title, /*html*/`<pre>${links}${noteLines}</pre>`);
 };
 

server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java

@@ -16,21 +16,33 @@ public class LJDiagnosticDTO {
     public final List<HintDTO> 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<String> messageNotes;
+    /** The places in the source that the message notes and hints name */
+    public final List<SourceReferenceDTO> 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<HintDTO> 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<HintDTO> hints,
+            String file, SourcePositionDTO position, List<String> messageNotes, List<SourceReferenceDTO> references) {
         this.category = category;
         this.type = type;
         this.title = title;
         this.message = message;
         this.hints = hints;
         this.file = file;
         this.position = position;
+        this.messageNotes = messageNotes;
+        this.references = references;
     }
 
     public static LJDiagnosticDTO from(LJDiagnostic diagnostic) {