From 56f86546d519d3f27d44af95cb932ce038b64ca0 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 19:27:22 +0000 Subject: [PATCH 1/4] Show the hints in the editor hover, with their code and line links VS Code's diagnostic hover is plain text and leaves the hints out, so the extension's hover now adds them in markdown over the error: code spans as inline code, the lines they name as links to that line, the rest escaped. The parsing of code spans and references moves to a module that the panel and the hover share, and so does the grouping of call sequences. Co-Authored-By: Claude Opus 5.5 --- client/src/services/hover.ts | 37 ++++++++++--- client/src/utils/message-markdown.spec.ts | 28 ++++++++++ client/src/utils/message-markdown.ts | 50 +++++++++++++++++ client/src/utils/message-text.ts | 65 +++++++++++++++++++++++ client/src/webview/message-text.ts | 36 +++---------- client/src/webview/views/sections.ts | 9 ++-- 6 files changed, 183 insertions(+), 42 deletions(-) create mode 100644 client/src/utils/message-markdown.spec.ts create mode 100644 client/src/utils/message-markdown.ts create mode 100644 client/src/utils/message-text.ts diff --git a/client/src/services/hover.ts b/client/src/services/hover.ts index cd96ea9..ac059ab 100644 --- a/client/src/services/hover.ts +++ b/client/src/services/hover.ts @@ -5,6 +5,8 @@ import { getSelectionContextVariables } from './context'; import { getOriginalVariableName, normalizeFilePath } from '../utils/utils'; import { definitionMatchesClass, getDefinitions } from './definition'; import { isExtensionRunning } from '../extension'; +import type { SourcePosition } from '../types/diagnostics'; +import { formatHintsMarkdown } from '../utils/message-markdown'; /** * Initializes hover provider for LiquidJava diagnostics @@ -29,12 +31,30 @@ export function registerHover() { } } - if (hoverContent.value.length === 0) return null; - return new vscode.Hover(hoverContent); + const contents = [hoverContent, ...getHoveredHints(document, position)].filter(content => content.value.length > 0); + if (contents.length === 0) return null; + return new vscode.Hover(contents); } }); } +/** + * The hints of the LiquidJava diagnostics at a position, in markdown. VS Code shows their message in its own hover, + * which is plain text, and that hover leaves the hints out + */ +function getHoveredHints(document: vscode.TextDocument, position: vscode.Position): vscode.MarkdownString[] { + const file = normalizeFilePath(document.uri.fsPath); + return (extension.diagnostics ?? []) + .filter(diagnostic => diagnostic.position && diagnostic.file && normalizeFilePath(diagnostic.file) === file) + .filter(diagnostic => { + const { lineStart, colStart, lineEnd, colEnd } = diagnostic.position!; + return new vscode.Range(lineStart, colStart, lineEnd, colEnd).contains(position); + }) + .map(diagnostic => formatHintsMarkdown(diagnostic.hints, diagnostic.references, toLocationLink)) + .filter((markdown): markdown is string => markdown !== null) + .map(markdown => new vscode.MarkdownString(markdown)); +} + function getHoveredVariable(document: vscode.TextDocument, position: vscode.Position): LJVariable | null { if (!extension.context) return null; @@ -120,9 +140,12 @@ function formatMethodHover(method: LJMethod): string { } function formatMethodLocationLink(method: LJMethod): string | null { - if (!method.position?.file) return null; - const uri = vscode.Uri.file(method.position.file).with({ - fragment: `L${method.position.lineStart + 1},${method.position.colStart + 1}` - }); - return `[Go to Refinements Definition](${uri.toString()})`; + const link = method.position && toLocationLink(method.position); + return link ? `[Go to Refinements Definition](${link})` : null; +} + +// a link that opens the file at the position +function toLocationLink(position: SourcePosition): string | null { + if (!position.file) return null; + return vscode.Uri.file(position.file).with({ fragment: `L${position.lineStart + 1},${position.colStart + 1}` }).toString(); } diff --git a/client/src/utils/message-markdown.spec.ts b/client/src/utils/message-markdown.spec.ts new file mode 100644 index 0000000..32ef7ef --- /dev/null +++ b/client/src/utils/message-markdown.spec.ts @@ -0,0 +1,28 @@ +import { describe, expect, it } from 'vitest'; +import { formatHintsMarkdown } from './message-markdown'; + +describe('hints in markdown', () => { + it('keeps the code and links the lines, and escapes the rest', () => { + const hint = '`preview.setTilingMode(int mode)` on line 51 decides the state of `preview`: with `mode == 2`, this call would be allowed'; + const position = { file: '/workspace/Stage.java', lineStart: 50, colStart: 8, lineEnd: 50, colEnd: 8 }; + const markdown = formatHintsMarkdown([ + { kind: 'deciding-argument', message: hint }, + { kind: 'general', message: "Call `` b.f('`') `` or `` `q `` when a*b < c_d | #e" }, + ], [{ message: hint, text: 'line 51', start: 37, position }], p => `file://${p.file}#L${p.lineStart + 1}`); + + expect(markdown).toBe([ + '**Hints**', + '`preview.setTilingMode(int mode)` on [line 51](file:///workspace/Stage.java#L51) decides the state of `preview`\\: with `mode == 2`\\, this call would be allowed', + "Call ``b.f('`')`` or `` `q `` when a\\*b \\< c\\_d \\| \\#e", + ].join('\n\n')); + }); + + it('lists several call sequences as options', () => { + const markdown = formatHintsMarkdown([ + { kind: 'call-sequence', message: 'Call `host.dispose()` before this call' }, + { kind: 'call-sequence', message: 'Call `host.removeNotify()` before this call' }, + ], [], () => null); + + expect(markdown).toBe('**Hints**\n\nAny one of these:\n\n- Call `host.dispose()` before this call\n- Call `host.removeNotify()` before this call'); + }); +}); diff --git a/client/src/utils/message-markdown.ts b/client/src/utils/message-markdown.ts new file mode 100644 index 0000000..8825bf2 --- /dev/null +++ b/client/src/utils/message-markdown.ts @@ -0,0 +1,50 @@ +import type { LJHint, LJSourceReference, SourcePosition } from "../types/diagnostics"; +import { groupHints, splitMessageText } from "./message-text"; + +// the link that opens a place in the source, or null if it has no file +export type LinkTarget = (position: SourcePosition) => string | null; + +/** + * Formats the hints of a diagnostic in markdown, as the panel shows them: their code as inline code and the places + * they name as links, with everything else escaped, since hints hold expressions with `*`, `_`, `<` or `|` + * @param references the places the hints name + * @param linkTo the link that opens a place + * @returns the markdown, or null if there are no hints + */ +export function formatHintsMarkdown(hints: LJHint[] | undefined, references: LJSourceReference[], linkTo: LinkTarget): string | null { + const { shown, options, notes } = groupHints(hints); + if (shown.length === 0) return null; + const format = (hint: LJHint) => formatMessageMarkdown(hint.message, references, linkTo); + return [ + shown.length === 1 ? "**Hint**" : "**Hints**", + ...options.length > 0 ? ["Any one of these:", options.map(hint => `- ${format(hint)}`).join("\n")] : [], + ...notes.map(format), + ].join("\n\n"); +} + +function formatMessageMarkdown(message: string, references: LJSourceReference[], linkTo: LinkTarget): string { + return splitMessageText(message, references).map(segment => { + switch (segment.kind) { + case "reference": { + const target = linkTo(segment.reference.position); + const text = escapeMarkdown(segment.reference.text); + return target ? `[${text}](${target})` : text; + } + case "code": return formatInlineCode(segment.code); + case "text": return escapeMarkdown(segment.text); + } + }).join(""); +} + +// a fence longer than any run of backticks in the code, and a space on each side, which markdown strips, if the code +// starts or ends with a backtick or a space +function formatInlineCode(code: string): string { + const fence = "`".repeat(Math.max(0, ...(code.match(/`+/g) ?? []).map(run => run.length)) + 1); + const pad = /^[`\s]|[`\s]$/.test(code) ? " " : ""; + return `${fence}${pad}${code}${pad}${fence}`; +} + +// every ASCII punctuation character can be escaped in markdown, so all are, rather than those that start a construct +function escapeMarkdown(text: string): string { + return text.replace(/[!-/:-@[-`{-~]/g, "\\$&"); +} diff --git a/client/src/utils/message-text.ts b/client/src/utils/message-text.ts new file mode 100644 index 0000000..451c975 --- /dev/null +++ b/client/src/utils/message-text.ts @@ -0,0 +1,65 @@ +import type { LJHint, LJSourceReference } from "../types/diagnostics"; + +// a part of a line of a diagnostic: plain text, code the verifier marks with backticks, or a place in the source it names +export type MessageSegment = + | { kind: "text"; text: string } + | { kind: "code"; code: string } + | { kind: "reference"; reference: LJSourceReference }; + +// 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)); + const segments: MessageSegment[] = []; + let text = ""; + const flushText = () => { + if (text) segments.push({ kind: "text", text }); + text = ""; + }; + let index = 0; + while (index < message.length) { + const link = links.find(reference => reference.start === index); + if (link) { + flushText(); + segments.push({ kind: "reference", reference: link }); + index += link.text.length; + continue; + } + CODE_SPAN.lastIndex = index; + const span = message[index] === "`" ? CODE_SPAN.exec(message) : null; + if (span) { + flushText(); + segments.push({ kind: "code", code: unpad(span[2]) }); + index += span[0].length; + continue; + } + text += message[index]; + index++; + } + flushText(); + return segments; +} + +// 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; +} + +/** + * The hints of a diagnostic as they are shown: several call sequences are alternatives, so they are listed as options + * apart from the hints that explain the error + */ +export function groupHints(hints: LJHint[] | undefined): { shown: LJHint[]; options: LJHint[]; notes: LJHint[] } { + const shown = (hints ?? []).filter(hint => hint.message.trim()); + const sequences = shown.filter(hint => hint.kind === "call-sequence"); + const options = sequences.length > 1 ? sequences : []; + const notes = options.length > 0 ? shown.filter(hint => hint.kind !== "call-sequence") : shown; + return { shown, options, notes }; +} diff --git a/client/src/webview/message-text.ts b/client/src/webview/message-text.ts index 595915f..bc69283 100644 --- a/client/src/webview/message-text.ts +++ b/client/src/webview/message-text.ts @@ -1,43 +1,21 @@ import type { LJSourceReference } from "../types/diagnostics"; +import { splitMessageText } from "../utils/message-text"; import { renderLineTags } from "./highlighting"; 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 += `${renderLineTags(unpad(span[2]))}`; - index += span[0].length; - continue; + return splitMessageText(message, references).map(segment => { + switch (segment.kind) { + case "reference": return renderReferenceLink(segment.reference); + case "code": return `${renderLineTags(segment.code)}`; + case "text": return escapeHtml(segment.text); } - 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; + }).join(""); } function renderReferenceLink(reference: LJSourceReference): string { diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index a571d57..da35aa4 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -4,6 +4,7 @@ import { renderHighlightedExpression, renderHighlightedInlineExpression } from " import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal"; import { renderCodicon, renderCodiconButton } from "../icons"; import { renderMessageText } from "../message-text"; +import { groupHints } from "../../utils/message-text"; import { LJVariable } from "../../types/context"; export const renderMainHeader = (title: string, selectedTab: NavTab, badges = NO_NAV_BADGES): string => /*html*/` @@ -32,23 +33,19 @@ export function setHintOpen(key: string, open: boolean) { /** * Renders the hints of a diagnostic, closed until the user opens them - * 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, references: LJSourceReference[] = []): string { - const shown = (hints ?? []).filter(hint => hint.message.trim()); + const { shown, options, notes } = groupHints(hints); if (shown.length === 0) return ''; - const options = shown.filter(hint => hint.kind === 'call-sequence'); - const listsOptions = options.length > 1; - const notes = listsOptions ? shown.filter(hint => hint.kind !== 'call-sequence') : shown; const open = key !== undefined && openHints.has(key); return /*html*/`
${shown.length === 1 ? 'Hint' : 'Hints'}
- ${listsOptions ? /*html*/` + ${options.length > 0 ? /*html*/`

Any one of these:

    ${options.map(hint => `
  • ${renderHintMessage(hint, references)}
    • `).join('')}
From 9b6502cc95c52ab1ec5ee25b3866d860b2952532 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 20:22:02 +0000 Subject: [PATCH 2/4] Hover: the error, its origin and its hints as one markdown card; panel code as in the hover The diagnostic message is now the headline alone, with the code it marks written without backticks, since VS Code shows that message as plain text (hover, Problems tab, problem view). The notes, the counterexample and the hints go to the extension's markdown part of the hover, with inline code and line links, as the hints already did. In the LiquidJava view, code in a message gets the look of inline code in a markdown hover (textCodeBlock.background) instead of the preformatted-text colours, which drew grey boxes around the Origin and Hint code in light themes. Co-Authored-By: Claude Fable 5.1 --- client/src/services/hover.ts | 12 +++--- client/src/utils/message-markdown.spec.ts | 27 +++++++++++++- client/src/utils/message-markdown.ts | 25 ++++++++++++- client/src/webview/styles.ts | 7 ++-- .../src/main/java/LJDiagnosticsHandler.java | 37 ++++++++++++++----- .../test/java/LJDiagnosticsHandlerTest.java | 13 +++---- 6 files changed, 92 insertions(+), 29 deletions(-) diff --git a/client/src/services/hover.ts b/client/src/services/hover.ts index ac059ab..d0ac596 100644 --- a/client/src/services/hover.ts +++ b/client/src/services/hover.ts @@ -6,7 +6,7 @@ import { getOriginalVariableName, normalizeFilePath } from '../utils/utils'; import { definitionMatchesClass, getDefinitions } from './definition'; import { isExtensionRunning } from '../extension'; import type { SourcePosition } from '../types/diagnostics'; -import { formatHintsMarkdown } from '../utils/message-markdown'; +import { formatDiagnosticMarkdown } from '../utils/message-markdown'; /** * Initializes hover provider for LiquidJava diagnostics @@ -31,7 +31,7 @@ export function registerHover() { } } - const contents = [hoverContent, ...getHoveredHints(document, position)].filter(content => content.value.length > 0); + const contents = [hoverContent, ...getHoveredDiagnostics(document, position)].filter(content => content.value.length > 0); if (contents.length === 0) return null; return new vscode.Hover(contents); } @@ -39,10 +39,10 @@ export function registerHover() { } /** - * The hints of the LiquidJava diagnostics at a position, in markdown. VS Code shows their message in its own hover, - * which is plain text, and that hover leaves the hints out + * What the LiquidJava diagnostics at a position say under their headline, in markdown: the notes that explain them, + * the counterexample and the hints. VS Code shows the headline in its own hover, which is plain text */ -function getHoveredHints(document: vscode.TextDocument, position: vscode.Position): vscode.MarkdownString[] { +function getHoveredDiagnostics(document: vscode.TextDocument, position: vscode.Position): vscode.MarkdownString[] { const file = normalizeFilePath(document.uri.fsPath); return (extension.diagnostics ?? []) .filter(diagnostic => diagnostic.position && diagnostic.file && normalizeFilePath(diagnostic.file) === file) @@ -50,7 +50,7 @@ function getHoveredHints(document: vscode.TextDocument, position: vscode.Positio const { lineStart, colStart, lineEnd, colEnd } = diagnostic.position!; return new vscode.Range(lineStart, colStart, lineEnd, colEnd).contains(position); }) - .map(diagnostic => formatHintsMarkdown(diagnostic.hints, diagnostic.references, toLocationLink)) + .map(diagnostic => formatDiagnosticMarkdown(diagnostic, toLocationLink)) .filter((markdown): markdown is string => markdown !== null) .map(markdown => new vscode.MarkdownString(markdown)); } diff --git a/client/src/utils/message-markdown.spec.ts b/client/src/utils/message-markdown.spec.ts index 32ef7ef..35d301d 100644 --- a/client/src/utils/message-markdown.spec.ts +++ b/client/src/utils/message-markdown.spec.ts @@ -1,5 +1,5 @@ import { describe, expect, it } from 'vitest'; -import { formatHintsMarkdown } from './message-markdown'; +import { formatDiagnosticMarkdown, formatHintsMarkdown } from './message-markdown'; describe('hints in markdown', () => { it('keeps the code and links the lines, and escapes the rest', () => { @@ -26,3 +26,28 @@ describe('hints in markdown', () => { expect(markdown).toBe('**Hints**\n\nAny one of these:\n\n- Call `host.dispose()` before this call\n- Call `host.removeNotify()` before this call'); }); }); + +describe('a diagnostic in markdown', () => { + it('shows the notes, then the counterexample, then the hints', () => { + const note = 'Origin: line 134, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`'; + const position = { file: '/workspace/M.java', lineStart: 133, colStart: 43, lineEnd: 133, colEnd: 43 }; + const diagnostic = { + category: 'error', type: 'refinement-error', title: 'Refinement Error', message: 'found `x` but expected `y`', + hints: [{ kind: 'general', message: 'Call `buffered.mark(int)` before this call' }], + file: '/workspace/M.java', position, messageNotes: [note], + references: [{ message: note, text: 'line 134', start: 8, position }], + expected: 'y', found: null, customMessage: '', declarationPosition: null, declarationPositions: [], declarationNotes: [], + counterexample: { assignments: [{ variable: 'x', value: '0' }, { variable: 'size(s)', value: '2' }] }, + } as unknown as import('../types/diagnostics').LJDiagnostic; + expect(formatDiagnosticMarkdown(diagnostic, p => `file://${p.file}#L${p.lineStart + 1}`)).toBe([ + 'Origin\\: [line 134](file:///workspace/M.java#L134)\\, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`', + 'Counterexample: `x == 0 && size(s) == 2`', + '**Hint**\n\nCall `buffered.mark(int)` before this call', + ].join('\n\n')); + }); + + it('is nothing when the diagnostic has no notes, counterexample or hints', () => { + const diagnostic = { category: 'error', type: 'custom-error', title: 'Error', message: 'm', hints: [], file: '', position: null, messageNotes: [], references: [] } as unknown as import('../types/diagnostics').LJDiagnostic; + expect(formatDiagnosticMarkdown(diagnostic, () => null)).toBeNull(); + }); +}); diff --git a/client/src/utils/message-markdown.ts b/client/src/utils/message-markdown.ts index 8825bf2..612df2d 100644 --- a/client/src/utils/message-markdown.ts +++ b/client/src/utils/message-markdown.ts @@ -1,9 +1,25 @@ -import type { LJHint, LJSourceReference, SourcePosition } from "../types/diagnostics"; +import type { LJDiagnostic, LJHint, LJSourceReference, SourcePosition } from "../types/diagnostics"; import { groupHints, splitMessageText } from "./message-text"; // the link that opens a place in the source, or null if it has no file export type LinkTarget = (position: SourcePosition) => string | null; +/** + * Formats what the editor hover shows of a diagnostic under its headline, in markdown: the notes that explain it + * (such as where a value comes from), the counterexample and the hints, with their code as inline code and the + * places they name as links. VS Code shows the headline itself in its own hover, which is plain text + * @param linkTo the link that opens a place + * @returns the markdown, or null if the diagnostic has none of them + */ +export function formatDiagnosticMarkdown(diagnostic: LJDiagnostic, linkTo: LinkTarget): string | null { + const parts = [ + ...diagnostic.messageNotes.map(note => formatMessageMarkdown(note, diagnostic.references, linkTo)), + formatCounterexampleMarkdown(diagnostic), + formatHintsMarkdown(diagnostic.hints, diagnostic.references, linkTo), + ].filter((part): part is string => part !== null && part.length > 0); + return parts.length > 0 ? parts.join("\n\n") : null; +} + /** * Formats the hints of a diagnostic in markdown, as the panel shows them: their code as inline code and the places * they name as links, with everything else escaped, since hints hold expressions with `*`, `_`, `<` or `|` @@ -22,6 +38,13 @@ export function formatHintsMarkdown(hints: LJHint[] | undefined, references: LJS ].join("\n\n"); } +// Counterexample: `x == 1 && y == 0`, as the verifier prints it, or null if the diagnostic has none +function formatCounterexampleMarkdown(diagnostic: LJDiagnostic): string | null { + if (diagnostic.type !== "refinement-error" || diagnostic.counterexample.assignments.length === 0) return null; + const assignments = diagnostic.counterexample.assignments.map(a => `${a.variable} == ${a.value}`).join(" && "); + return `Counterexample: ${formatInlineCode(assignments)}`; +} + function formatMessageMarkdown(message: string, references: LJSourceReference[], linkTo: LinkTarget): string { return splitMessageText(message, references).map(segment => { switch (segment.kind) { diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index c85bdc1..5c1e47d 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -233,14 +233,13 @@ export function getStyles(): string { background-color: var(--vscode-editor-background); border-radius: 4px; } - /* code that a message marks with backticks, set apart from its prose */ + /* code that a message marks with backticks, as VS Code renders inline code in a markdown hover */ .lj-code { - padding: 0 0.2em; + padding: 0 0.1em; 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); + background-color: var(--vscode-textCodeBlock-background); overflow-wrap: break-word; } .message-note { diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java index b638a2f..fb60911 100644 --- a/server/src/main/java/LJDiagnosticsHandler.java +++ b/server/src/main/java/LJDiagnosticsHandler.java @@ -2,6 +2,8 @@ import java.util.Collections; import java.util.List; import java.util.Map; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -82,20 +84,37 @@ public static List getDiagnostics(List d .toList(); } + /** A run of backticks, the code, and a run of the same length, as the verifier marks code in its messages */ + private static final Pattern CODE_SPAN = Pattern.compile("(`+)([\\s\\S]+?)(? lines = new ArrayList<>(); - lines.add(String.format("%s: %s", diagnostic.getTitle(), diagnostic.getMessage())); - lines.addAll(diagnostic.getMessageNotes()); - String counterexample = diagnostic.getCounterexampleStr(); - if (counterexample != null && !counterexample.isBlank()) - lines.add(counterexample); - return String.join("\n", lines); + return String.format("%s: %s", diagnostic.getTitle(), plainCode(diagnostic.getMessage())); + } + + /** The text with the code it marks with backticks written without them */ + static String plainCode(String text) { + if (text == null) + return ""; + Matcher matcher = CODE_SPAN.matcher(text); + StringBuilder plain = new StringBuilder(); + while (matcher.find()) + matcher.appendReplacement(plain, Matcher.quoteReplacement(unpad(matcher.group(2)))); + matcher.appendTail(plain); + return plain.toString(); + } + + // the code without the space on each side that the verifier adds to code with a backtick or a space at an end + private static String unpad(String code) { + return code.length() >= 2 && code.startsWith(" ") && code.endsWith(" ") ? code.substring(1, code.length() - 1) + : code; } /** diff --git a/server/src/test/java/LJDiagnosticsHandlerTest.java b/server/src/test/java/LJDiagnosticsHandlerTest.java index 18f0b20..478c776 100644 --- a/server/src/test/java/LJDiagnosticsHandlerTest.java +++ b/server/src/test/java/LJDiagnosticsHandlerTest.java @@ -10,9 +10,9 @@ class LJDiagnosticsHandlerTest { @Test - void hoverShowsTheHeadlineThenTheNotesThenTheCounterexampleButNoHints() { - LJDiagnostic diagnostic = new LJDiagnostic("Refinement Error", "expected timeout >= 0 but could not prove it", - null, "", null) { + void messageIsTheHeadlineWithItsCodeUnwrappedAndNothingElse() { + LJDiagnostic diagnostic = new LJDiagnostic("Refinement Error", + "found `x > 0 && y == 1` but expected `` `q `` and `a*b`", null, "", null) { @Override public List getMessageNotes() { return List.of("where Positive(x) means x > 0"); @@ -20,10 +20,7 @@ public List getMessageNotes() { }; diagnostic.setCounterexampleStr("Counterexample: timeout == -1"); diagnostic.addHint(Hint.general("Add a refinement")); - - assertEquals(""" - Refinement Error: expected timeout >= 0 but could not prove it - where Positive(x) means x > 0 - Counterexample: timeout == -1""", LJDiagnosticsHandler.getHoverMessage(diagnostic)); + assertEquals("Refinement Error: found x > 0 && y == 1 but expected `q and a*b", + LJDiagnosticsHandler.getHoverMessage(diagnostic)); } } From 5a6413c06ded6a7ba213d898204fa72b91cf2001 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 20:25:36 +0000 Subject: [PATCH 3/4] Name the diagnostic message for what it is It is the text of the Problems tab, the problem view and the hover's problem part, not of the hover alone. Co-Authored-By: Claude Fable 5.1 --- server/src/main/java/LJDiagnosticsHandler.java | 4 ++-- server/src/test/java/LJDiagnosticsHandlerTest.java | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java index fb60911..015596b 100644 --- a/server/src/main/java/LJDiagnosticsHandler.java +++ b/server/src/main/java/LJDiagnosticsHandler.java @@ -74,7 +74,7 @@ public static List getDiagnostics(List d d -> PathUtils.toFileUri(d.getFile()), Collectors.mapping(d -> { Range range = getRangeFromPosition(d.getPosition()); - return new Diagnostic(range, getHoverMessage(d), severity, SOURCE); + return new Diagnostic(range, diagnosticMessage(d), severity, SOURCE); }, Collectors.toList()) )); @@ -95,7 +95,7 @@ public static List getDiagnostics(List d * @param diagnostic the diagnostic * @return the message */ - static String getHoverMessage(LJDiagnostic diagnostic) { + static String diagnosticMessage(LJDiagnostic diagnostic) { return String.format("%s: %s", diagnostic.getTitle(), plainCode(diagnostic.getMessage())); } diff --git a/server/src/test/java/LJDiagnosticsHandlerTest.java b/server/src/test/java/LJDiagnosticsHandlerTest.java index 478c776..6488e7e 100644 --- a/server/src/test/java/LJDiagnosticsHandlerTest.java +++ b/server/src/test/java/LJDiagnosticsHandlerTest.java @@ -21,6 +21,6 @@ public List getMessageNotes() { diagnostic.setCounterexampleStr("Counterexample: timeout == -1"); diagnostic.addHint(Hint.general("Add a refinement")); assertEquals("Refinement Error: found x > 0 && y == 1 but expected `q and a*b", - LJDiagnosticsHandler.getHoverMessage(diagnostic)); + LJDiagnosticsHandler.diagnosticMessage(diagnostic)); } } From acbeda28fe0a500d884c085cccaad5101201b847 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 11 Nov 2026 20:34:08 +0000 Subject: [PATCH 4/4] Hover: the headline in the markdown card too; the diagnostic keeps its title The PM wants the error, its origin and its hints all rendered alike. The diagnostic's message is now the title alone, so the Problems tab and the problem view show the error type, and the card under it shows the headline with its code as inline code. Co-Authored-By: Claude Fable 5.1 --- client/src/utils/message-markdown.spec.ts | 9 +++--- client/src/utils/message-markdown.ts | 9 +++--- .../src/main/java/LJDiagnosticsHandler.java | 32 +++---------------- .../test/java/LJDiagnosticsHandlerTest.java | 9 +++--- 4 files changed, 18 insertions(+), 41 deletions(-) diff --git a/client/src/utils/message-markdown.spec.ts b/client/src/utils/message-markdown.spec.ts index 35d301d..d81bdf2 100644 --- a/client/src/utils/message-markdown.spec.ts +++ b/client/src/utils/message-markdown.spec.ts @@ -28,7 +28,7 @@ describe('hints in markdown', () => { }); describe('a diagnostic in markdown', () => { - it('shows the notes, then the counterexample, then the hints', () => { + it('shows the headline, then the notes, then the counterexample, then the hints', () => { const note = 'Origin: line 134, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`'; const position = { file: '/workspace/M.java', lineStart: 133, colStart: 43, lineEnd: 133, colEnd: 43 }; const diagnostic = { @@ -40,14 +40,15 @@ describe('a diagnostic in markdown', () => { counterexample: { assignments: [{ variable: 'x', value: '0' }, { variable: 'size(s)', value: '2' }] }, } as unknown as import('../types/diagnostics').LJDiagnostic; expect(formatDiagnosticMarkdown(diagnostic, p => `file://${p.file}#L${p.lineStart + 1}`)).toBe([ + 'found `x` but expected `y`', 'Origin\\: [line 134](file:///workspace/M.java#L134)\\, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`', 'Counterexample: `x == 0 && size(s) == 2`', '**Hint**\n\nCall `buffered.mark(int)` before this call', ].join('\n\n')); }); - it('is nothing when the diagnostic has no notes, counterexample or hints', () => { - const diagnostic = { category: 'error', type: 'custom-error', title: 'Error', message: 'm', hints: [], file: '', position: null, messageNotes: [], references: [] } as unknown as import('../types/diagnostics').LJDiagnostic; - expect(formatDiagnosticMarkdown(diagnostic, () => null)).toBeNull(); + it('is the headline alone when the diagnostic has no notes, counterexample or hints', () => { + const diagnostic = { category: 'error', type: 'custom-error', title: 'Error', message: 'a < b', hints: [], file: '', position: null, messageNotes: [], references: [] } as unknown as import('../types/diagnostics').LJDiagnostic; + expect(formatDiagnosticMarkdown(diagnostic, () => null)).toBe('a \\< b'); }); }); diff --git a/client/src/utils/message-markdown.ts b/client/src/utils/message-markdown.ts index 612df2d..e148824 100644 --- a/client/src/utils/message-markdown.ts +++ b/client/src/utils/message-markdown.ts @@ -5,14 +5,15 @@ import { groupHints, splitMessageText } from "./message-text"; export type LinkTarget = (position: SourcePosition) => string | null; /** - * Formats what the editor hover shows of a diagnostic under its headline, in markdown: the notes that explain it - * (such as where a value comes from), the counterexample and the hints, with their code as inline code and the - * places they name as links. VS Code shows the headline itself in its own hover, which is plain text + * Formats what the editor hover shows of a diagnostic, in markdown: its headline, the notes that explain it (such as + * where a value comes from), the counterexample and the hints, with their code as inline code and the places they + * name as links. VS Code's own part of the hover, which is plain text, shows only the diagnostic's title * @param linkTo the link that opens a place - * @returns the markdown, or null if the diagnostic has none of them + * @returns the markdown, or null if the diagnostic has no headline */ export function formatDiagnosticMarkdown(diagnostic: LJDiagnostic, linkTo: LinkTarget): string | null { const parts = [ + formatMessageMarkdown(diagnostic.message, diagnostic.references, linkTo), ...diagnostic.messageNotes.map(note => formatMessageMarkdown(note, diagnostic.references, linkTo)), formatCounterexampleMarkdown(diagnostic), formatHintsMarkdown(diagnostic.hints, diagnostic.references, linkTo), diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java index 015596b..4f3fac7 100644 --- a/server/src/main/java/LJDiagnosticsHandler.java +++ b/server/src/main/java/LJDiagnosticsHandler.java @@ -2,8 +2,6 @@ import java.util.Collections; import java.util.List; import java.util.Map; -import java.util.regex.Matcher; -import java.util.regex.Pattern; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -84,37 +82,15 @@ public static List getDiagnostics(List d .toList(); } - /** A run of backticks, the code, and a run of the same length, as the verifier marks code in its messages */ - private static final Pattern CODE_SPAN = Pattern.compile("(`+)([\\s\\S]+?)(?= 2 && code.startsWith(" ") && code.endsWith(" ") ? code.substring(1, code.length() - 1) - : code; + return diagnostic.getTitle(); } /** diff --git a/server/src/test/java/LJDiagnosticsHandlerTest.java b/server/src/test/java/LJDiagnosticsHandlerTest.java index 6488e7e..c585785 100644 --- a/server/src/test/java/LJDiagnosticsHandlerTest.java +++ b/server/src/test/java/LJDiagnosticsHandlerTest.java @@ -10,9 +10,9 @@ class LJDiagnosticsHandlerTest { @Test - void messageIsTheHeadlineWithItsCodeUnwrappedAndNothingElse() { - LJDiagnostic diagnostic = new LJDiagnostic("Refinement Error", - "found `x > 0 && y == 1` but expected `` `q `` and `a*b`", null, "", null) { + void messageIsTheTitleAlone() { + LJDiagnostic diagnostic = new LJDiagnostic("Refinement Error", "found `x > 0` but expected `y == 1`", null, "", + null) { @Override public List getMessageNotes() { return List.of("where Positive(x) means x > 0"); @@ -20,7 +20,6 @@ public List getMessageNotes() { }; diagnostic.setCounterexampleStr("Counterexample: timeout == -1"); diagnostic.addHint(Hint.general("Add a refinement")); - assertEquals("Refinement Error: found x > 0 && y == 1 but expected `q and a*b", - LJDiagnosticsHandler.diagnosticMessage(diagnostic)); + assertEquals("Refinement Error", LJDiagnosticsHandler.diagnosticMessage(diagnostic)); } }