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

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

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

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, 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*/`
                     <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) {

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<SourceReferenceDTO> from(List<SourceReference> references) {
+        return references.stream().map(SourceReferenceDTO::from).toList();
+    }
+}

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