Problems says what is wrong, hover details by setting, a tab for showView

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",

client/src/services/hover.ts

@@ -39,25 +39,29 @@ 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)
         .filter(diagnostic => {
             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<boolean>('liquidjava.hover.showHints', true);
+// 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 {
+    const configuration = vscode.workspace.getConfiguration();
+    return configuration.get<boolean>('liquidjava.hover.showDetails', true) && configuration.get<boolean>('liquidjava.hover.showHints', true);
 }
 
 function getHoveredVariable(document: vscode.TextDocument, position: vscode.Position): LJVariable | null {

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

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

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

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

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;

server/src/main/java/LJDiagnosticsHandler.java

@@ -83,14 +83,16 @@ public static List<PublishDiagnosticsParams> getDiagnostics(List<LJDiagnostic> 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;
     }
 
     /**

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