From 56d9ff9d81a034c9f1b0f655e00a69ffcb566a5b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 12 Nov 2026 02:11:05 +0000 Subject: [PATCH 1/2] Problems says what is wrong, the hover's details by setting, and a tab for the showView command The Problems entry of an error was its title alone ("State Refinement Error"), so the list said which kind of error there was and not what was wrong. The language server now sends the title and the headline, as plain text; the extension's part of the hover no longer repeats the headline and shows the details only: the origin notes, the counterexample and the hints. liquidjava.hover.showDetails replaces liquidjava.hover.showHints (0.1.1): off, the hover is the message alone and every detail is in the LiquidJava view. A hover that named the hints without showing them was neither one thing nor the other. liquidjava.showView takes a tab without a diagnostic, which opens that tab of the view, and a third argument naming who asked, for the usage log (the code lenses by default). Co-Authored-By: Claude Fable 5.1 --- client/package.json | 4 ++-- client/src/services/hover.ts | 14 +++++++------ client/src/services/webview.ts | 21 +++++++++++++++---- client/src/utils/message-markdown.spec.ts | 16 ++++---------- client/src/utils/message-markdown.ts | 21 +++++++------------ client/src/webview/script.spec.ts | 12 +++++++++++ client/src/webview/script.ts | 5 +++++ .../src/main/java/LJDiagnosticsHandler.java | 10 +++++---- .../test/java/LJDiagnosticsHandlerTest.java | 4 ++-- 9 files changed, 63 insertions(+), 44 deletions(-) diff --git a/client/package.json b/client/package.json index dbd7ba0..939998d 100644 --- a/client/package.json +++ b/client/package.json @@ -65,10 +65,10 @@ "default": true, "description": "Apply italic style to LiquidJava injected tokens on top of any active theme" }, - "liquidjava.hover.showHints": { + "liquidjava.hover.showDetails": { "type": "boolean", "default": true, - "description": "Show the hints of an error in the editor hover. When off, the hover says that the hints are in the LiquidJava view, where they stay closed until opened." + "description": "Show the details of an error in the editor hover under its message: the origin notes, the counterexample and the hints. When off, the hover shows the message alone and the details are in the LiquidJava view, where the hints stay closed until opened." }, "liquidjava.usageLog": { "type": "string", diff --git a/client/src/services/hover.ts b/client/src/services/hover.ts index 6c669b0..9440631 100644 --- a/client/src/services/hover.ts +++ b/client/src/services/hover.ts @@ -39,10 +39,12 @@ export function registerHover() { } /** - * 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 + * The details of the LiquidJava diagnostics at a position, in markdown: the notes that explain them, the + * counterexample and the hints. VS Code shows the message itself in its own part of the hover, which is plain text. + * Nothing when liquidjava.hover.showDetails is off: the details are then in the LiquidJava view only */ function getHoveredDiagnostics(document: vscode.TextDocument, position: vscode.Position): vscode.MarkdownString[] { + if (!showDetailsInHover()) return []; const file = normalizeFilePath(document.uri.fsPath); return (extension.diagnostics ?? []) .filter(diagnostic => diagnostic.position && diagnostic.file && normalizeFilePath(diagnostic.file) === file) @@ -50,14 +52,14 @@ function getHoveredDiagnostics(document: vscode.TextDocument, position: vscode.P const { lineStart, colStart, lineEnd, colEnd } = diagnostic.position!; return new vscode.Range(lineStart, colStart, lineEnd, colEnd).contains(position); }) - .map(diagnostic => formatDiagnosticMarkdown(diagnostic, toLocationLink, { hints: showHintsInHover() })) + .map(diagnostic => formatDiagnosticMarkdown(diagnostic, toLocationLink)) .filter((markdown): markdown is string => markdown !== null) .map(markdown => new vscode.MarkdownString(markdown)); } -// liquidjava.hover.showHints: off keeps the hints in the view only, closed until opened (user studies) -function showHintsInHover(): boolean { - return vscode.workspace.getConfiguration().get('liquidjava.hover.showHints', true); +// liquidjava.hover.showDetails: off keeps the origin notes, the counterexample and the hints in the view only (user studies) +function showDetailsInHover(): boolean { + return vscode.workspace.getConfiguration().get('liquidjava.hover.showDetails', true); } function getHoveredVariable(document: vscode.TextDocument, position: vscode.Position): LJVariable | null { diff --git a/client/src/services/webview.ts b/client/src/services/webview.ts index ce1d406..d275097 100644 --- a/client/src/services/webview.ts +++ b/client/src/services/webview.ts @@ -12,6 +12,7 @@ import { logUsage } from "./usage-log"; export function registerWebview(context: vscode.ExtensionContext) { extension.webview = new LiquidJavaWebviewProvider(context.extensionUri); let pendingDiagnosticReveal: { diagnostic: DiagnosticRevealTarget, tab?: NavTab } | undefined; + let pendingTab: NavTab | undefined; // webview provider context.subscriptions.push( @@ -20,13 +21,21 @@ export function registerWebview(context: vscode.ExtensionContext) { ); // show view command context.subscriptions.push( - // shows the diagnostic in the Verification tab, or a state error in the State Machine tab when tab is 'fsm' - vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget, tab?: NavTab) => { + // shows the diagnostic in the Verification tab, or a state error in the State Machine tab when tab is 'fsm'; + // without a diagnostic, opens the tab, if one is given. from names the caller in the usage log: the code + // lenses above an error (the default), or another extension + vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget, tab?: NavTab, from = 'code-lens') => { const isVisible = extension.webview?.isVisible(); await vscode.commands.executeCommand("liquidJavaView.focus"); - if (!diagnostic) return; + if (!diagnostic) { + if (!tab) return; + logUsage('tab', { tab, from }); + if (isVisible) extension.webview?.sendMessage({ type: "selectTab", tab }); + else pendingTab = tab; + return; + } // the code lenses above an error: its title opens the Verification tab, "Show in state machine" the State Machine tab - logUsage(tab === 'fsm' ? 'state-machine' : 'show-view', { from: 'code-lens', file: diagnostic.file, line: diagnostic.position.lineStart + 1 }); + logUsage(tab === 'fsm' ? 'state-machine' : 'show-view', { from, file: diagnostic.file, line: diagnostic.position.lineStart + 1 }); if (isVisible) { extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic, tab }); @@ -48,6 +57,10 @@ export function registerWebview(context: vscode.ExtensionContext) { extension.webview?.sendMessage({ type: "revealDiagnostic", ...pendingDiagnosticReveal }); pendingDiagnosticReveal = undefined; } + if (pendingTab) { + extension.webview?.sendMessage({ type: "selectTab", tab: pendingTab }); + pendingTab = undefined; + } } }) ); diff --git a/client/src/utils/message-markdown.spec.ts b/client/src/utils/message-markdown.spec.ts index 31e510b..b88cdda 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 { HINTS_IN_VIEW, formatDiagnosticMarkdown, 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', () => { @@ -28,7 +28,7 @@ describe('hints in markdown', () => { }); describe('a diagnostic in markdown', () => { - it('shows the headline, then the notes, then the counterexample, then the hints', () => { + it('shows the notes, then the counterexample, then the hints, and not the headline, which VS Code shows', () => { 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,22 +40,14 @@ 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('says where the hints are instead of showing them when hints are off (liquidjava.hover.showHints)', () => { - const withHints = { category: 'error', type: 'custom-error', title: 'Error', message: 'a < b', hints: [{ kind: 'general', message: 'Call `f()` first' }], file: '', position: null, messageNotes: [], references: [] } as unknown as import('../types/diagnostics').LJDiagnostic; - expect(formatDiagnosticMarkdown(withHints, () => null, { hints: false })).toBe('a \\< b\n\n' + HINTS_IN_VIEW); - const without = { ...withHints, hints: [] } as unknown as import('../types/diagnostics').LJDiagnostic; - expect(formatDiagnosticMarkdown(without, () => null, { hints: false })).toBe('a \\< b'); - }); - - it('is the headline alone when the diagnostic has no notes, counterexample or hints', () => { + it('is null 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'); + expect(formatDiagnosticMarkdown(diagnostic, () => null)).toBeNull(); }); }); diff --git a/client/src/utils/message-markdown.ts b/client/src/utils/message-markdown.ts index ea734bb..b663b05 100644 --- a/client/src/utils/message-markdown.ts +++ b/client/src/utils/message-markdown.ts @@ -4,26 +4,19 @@ 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; -// what the hover says instead of the hints when liquidjava.hover.showHints is off -export const HINTS_IN_VIEW = "**Hints**: in the LiquidJava view (Hints, under the error)."; - /** - * 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 + * Formats the details the editor hover shows under a diagnostic's message, 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. The message itself is not repeated: VS Code's own part of the hover shows it, as plain text, + * from the Problems entry * @param linkTo the link that opens a place - * @param options hints: false leaves the hints out and says where they are (the LiquidJava view) when there are any - * @returns the markdown, or null if the diagnostic has no headline + * @returns the markdown, or null if the diagnostic has no details */ -export function formatDiagnosticMarkdown(diagnostic: LJDiagnostic, linkTo: LinkTarget, options: { hints?: boolean } = {}): string | null { - const hints = options.hints === false - ? diagnostic.hints && diagnostic.hints.length > 0 ? HINTS_IN_VIEW : null - : formatHintsMarkdown(diagnostic.hints, diagnostic.references, linkTo); +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), - hints, + 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; } diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index df0f2cb..688cede 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -200,6 +200,18 @@ describe('webview script', () => { ]); }); + it('opens a tab on a selectTab message (the liquidjava.showView command with a tab and no diagnostic)', () => { + showDiagnostics([diagnostic(currentFile, 'Current error')]); + receive({ type: 'fsm', sms: [stateMachine] }); + postMessage.mockClear(); + + receive({ type: 'selectTab', tab: 'fsm' }); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('fsm'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('Counter'); + // the extension host logs that use itself, with who asked for it + expect(postMessage.mock.calls.filter(([m]) => (m as { type: string }).type === 'usage')).toEqual([]); + }); + it('opens a state error focused on the error and toggles the dimming', () => { const error = stateError('State refinement error', errorMachine('Counter', 'close')); showDiagnostics([error]); diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 8ded3b9..87503b5 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -421,6 +421,11 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) followCursorStateError(msg.errorAtCursor as LJDiagnostic | undefined); if (selectedTab === 'context') updateView(); break; + case 'selectTab': { // the liquidjava.showView command with a tab and no diagnostic + const tab = msg.tab as NavTab; + if (tab !== selectedTab) { selectedTab = tab; updateView(); } + break; + } case 'revealDiagnostic': { const revealTarget = msg.diagnostic as DiagnosticRevealTarget; const stateError = msg.tab === 'fsm' ? findStateErrorAt(revealTarget) : undefined; diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java index 4f3fac7..86d737b 100644 --- a/server/src/main/java/LJDiagnosticsHandler.java +++ b/server/src/main/java/LJDiagnosticsHandler.java @@ -83,14 +83,16 @@ public static List getDiagnostics(List d } /** - * The message of a diagnostic in the editor: its title alone. VS Code shows that message as plain text in the - * hover, the Problems tab and the problem view; the headline, the notes, the counterexample and the hints are - * rendered by the extension's own part of the hover, in markdown, and by the LiquidJava view + * The message of a diagnostic in the editor: its title and its headline, as plain text, so the Problems tab says + * what is wrong and not only which kind of error it is. VS Code shows that message as plain text in the hover, the + * Problems tab and the problem view; the notes, the counterexample and the hints are rendered by the extension's + * own part of the hover, in markdown, and by the LiquidJava view * @param diagnostic the diagnostic * @return the message */ static String diagnosticMessage(LJDiagnostic diagnostic) { - return diagnostic.getTitle(); + String headline = diagnostic.getMessage() == null ? "" : diagnostic.getMessage().replace("`", "").trim(); + return headline.isEmpty() ? diagnostic.getTitle() : diagnostic.getTitle() + ": " + headline; } /** diff --git a/server/src/test/java/LJDiagnosticsHandlerTest.java b/server/src/test/java/LJDiagnosticsHandlerTest.java index c585785..0dea557 100644 --- a/server/src/test/java/LJDiagnosticsHandlerTest.java +++ b/server/src/test/java/LJDiagnosticsHandlerTest.java @@ -10,7 +10,7 @@ class LJDiagnosticsHandlerTest { @Test - void messageIsTheTitleAlone() { + void messageIsTheTitleAndTheHeadlineWithoutCodeFences() { LJDiagnostic diagnostic = new LJDiagnostic("Refinement Error", "found `x > 0` but expected `y == 1`", null, "", null) { @Override @@ -20,6 +20,6 @@ public List getMessageNotes() { }; diagnostic.setCounterexampleStr("Counterexample: timeout == -1"); diagnostic.addHint(Hint.general("Add a refinement")); - assertEquals("Refinement Error", LJDiagnosticsHandler.diagnosticMessage(diagnostic)); + assertEquals("Refinement Error: found x > 0 but expected y == 1", LJDiagnosticsHandler.diagnosticMessage(diagnostic)); } } From eb980279d95555724793074471654c6880b1b0d8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 12 Nov 2026 02:15:13 +0000 Subject: [PATCH 2/2] The hover honours 0.1.1's showHints key when a settings file turns it off Co-Authored-By: Claude Fable 5.1 --- client/src/services/hover.ts | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/client/src/services/hover.ts b/client/src/services/hover.ts index 9440631..e495d8d 100644 --- a/client/src/services/hover.ts +++ b/client/src/services/hover.ts @@ -57,9 +57,11 @@ function getHoveredDiagnostics(document: vscode.TextDocument, position: vscode.P .map(markdown => new vscode.MarkdownString(markdown)); } -// liquidjava.hover.showDetails: off keeps the origin notes, the counterexample and the hints in the view only (user studies) +// liquidjava.hover.showDetails: off keeps the origin notes, the counterexample and the hints in the view only (user +// studies). liquidjava.hover.showHints, its name in 0.1.1, still counts when a settings file sets it to false function showDetailsInHover(): boolean { - return vscode.workspace.getConfiguration().get('liquidjava.hover.showDetails', true); + const configuration = vscode.workspace.getConfiguration(); + return configuration.get('liquidjava.hover.showDetails', true) && configuration.get('liquidjava.hover.showHints', true); } function getHoveredVariable(document: vscode.TextDocument, position: vscode.Position): LJVariable | null {