Hints out of the hover by setting, and a usage log of the view for user studies

client/package.json

@@ -64,6 +64,16 @@
 					"type": "boolean",
 					"default": true,
 					"description": "Apply italic style to LiquidJava injected tokens on top of any active theme"
+				},
+				"liquidjava.hover.showHints": {
+					"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."
+				},
+				"liquidjava.usageLog": {
+					"type": "string",
+					"default": "",
+					"description": "Path of a JSON Lines file to which the extension appends what is used in the LiquidJava view: tabs, hints opened, Found steps, locations, state machine, copies. Empty: nothing is written. Meant for user studies."
 				}
 			}
 		},

client/src/extension.ts

@@ -7,6 +7,7 @@ import { registerCommands } from "./services/commands";
 import { registerStatusBar, updateStatusBar } from "./services/status-bar";
 import { registerWebview } from "./services/webview";
 import { registerHover } from "./services/hover";
+import { registerUsageLog } from "./services/usage-log";
 import { registerEvents } from "./services/events";
 import { registerAutocomplete } from "./services/autocomplete";
 import { refreshCodeLenses, registerCodeLens } from "./services/codelens";
@@ -27,6 +28,7 @@ export async function activate(context: vscode.ExtensionContext): Promise<Liquid
     registerCommands(context);
     registerEvents(context);
     registerWebview(context);
+    registerUsageLog(context);
     registerAutocomplete(context);
     registerCodeLens(context);
     registerHover();

client/src/services/hover.ts

@@ -50,11 +50,16 @@ 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))
+        .map(diagnostic => formatDiagnosticMarkdown(diagnostic, toLocationLink, { hints: showHintsInHover() }))
         .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);
+}
+
 function getHoveredVariable(document: vscode.TextDocument, position: vscode.Position): LJVariable | null {
     if (!extension.context) return null;
 

client/src/services/usage-log.ts

@@ -0,0 +1,55 @@
+import * as vscode from "vscode";
+import * as fs from "fs";
+import * as path from "path";
+import { extension } from "../state";
+import { formatUsageLine, usageEventFor, type UsageEvent } from "../utils/usage-log";
+
+const SETTING = "liquidjava.usageLog";
+
+/**
+ * Appends what is used in the LiquidJava view to the file named by liquidjava.usageLog (JSON Lines),
+ * for user studies. Nothing is written when the setting is empty. A failure to write never reaches the user.
+ * @param context The extension context
+ */
+export function registerUsageLog(context: vscode.ExtensionContext) {
+    let file = currentFile();
+    context.subscriptions.push(vscode.workspace.onDidChangeConfiguration(e => {
+        if (e.affectsConfiguration(SETTING)) file = currentFile();
+    }));
+    if (extension.webview) {
+        context.subscriptions.push(extension.webview.onDidReceiveMessage(message => {
+            const event = usageEventFor(message);
+            if (event) append(file, event);
+        }));
+    }
+}
+
+/**
+ * Logs a use that does not come through the webview, such as the "Show in state machine" code lens
+ * @param event what was used
+ * @param detail the fields of the line
+ */
+export function logUsage(event: string, detail: Record<string, unknown> = {}) {
+    append(currentFile(), { t: new Date().toISOString(), event, ...detail });
+}
+
+function currentFile(): string | null {
+    const value = vscode.workspace.getConfiguration().get<string>(SETTING, "").trim();
+    return value.length > 0 ? value : null;
+}
+
+// the writes are asynchronous, so a slow disk never stalls the extension host, and chained, so the lines keep their order
+let pending: Promise<void> = Promise.resolve();
+
+function append(file: string | null, event: UsageEvent) {
+    if (!file) return;
+    const line = formatUsageLine(event);
+    pending = pending.then(async () => {
+        try {
+            await fs.promises.mkdir(path.dirname(file), { recursive: true });
+            await fs.promises.appendFile(file, line);
+        } catch (error) {
+            extension.logger?.client.error(`usage log: cannot write ${file}: ${String(error)}`);
+        }
+    });
+}

client/src/services/webview.ts

@@ -3,6 +3,7 @@ import { LiquidJavaWebviewProvider } from "../webview/provider";
 import { extension } from "../state";
 import type { DiagnosticRevealTarget } from "../types/diagnostics";
 import type { NavTab } from "../webview/views/sections";
+import { logUsage } from "./usage-log";
 
 /**
  * Initializes the webview panel for the extension
@@ -23,7 +24,9 @@ export function registerWebview(context: vscode.ExtensionContext) {
         vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget, tab?: NavTab) => {
             const isVisible = extension.webview?.isVisible();
             await vscode.commands.executeCommand("liquidJavaView.focus");
-            if (!diagnostic) return; 
+            if (!diagnostic) 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 });
 
             if (isVisible) {
                 extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic, tab });

client/src/utils/message-markdown.spec.ts

@@ -1,5 +1,5 @@
 import { describe, expect, it } from 'vitest';
-import { formatDiagnosticMarkdown, formatHintsMarkdown } from './message-markdown';
+import { HINTS_IN_VIEW, formatDiagnosticMarkdown, formatHintsMarkdown } from './message-markdown';
 
 describe('hints in markdown', () => {
     it('keeps the code and links the lines, and escapes the rest', () => {
@@ -47,6 +47,13 @@ describe('a diagnostic in markdown', () => {
         ].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', () => {
         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');

client/src/utils/message-markdown.ts

@@ -4,19 +4,26 @@ 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
  * @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
  */
-export function formatDiagnosticMarkdown(diagnostic: LJDiagnostic, linkTo: LinkTarget): string | null {
+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);
     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),
+        hints,
     ].filter((part): part is string => part !== null && part.length > 0);
     return parts.length > 0 ? parts.join("\n\n") : null;
 }

client/src/utils/usage-log.spec.ts

@@ -0,0 +1,21 @@
+import { describe, expect, it } from 'vitest';
+import { formatUsageLine, usageEventFor } from './usage-log';
+
+describe('the usage log', () => {
+    const now = new Date('2026-11-12T10:00:00.000Z');
+
+    it('turns a usage message into a line with the time, the action as event, and its details', () => {
+        expect(usageEventFor({ type: 'usage', action: 'tab', tab: 'fsm' }, now))
+            .toEqual({ t: '2026-11-12T10:00:00.000Z', event: 'tab', tab: 'fsm' });
+        expect(formatUsageLine(usageEventFor({ type: 'usage', action: 'hints', open: true, error: 'e1' }, now)!))
+            .toBe('{"t":"2026-11-12T10:00:00.000Z","event":"hints","open":true,"error":"e1"}\n');
+    });
+
+    it('logs a click on a location as location, and nothing for the other messages', () => {
+        expect(usageEventFor({ type: 'openFile', filePath: '/w/M.java', line: 12, character: 4 }, now))
+            .toEqual({ t: '2026-11-12T10:00:00.000Z', event: 'location', file: '/w/M.java', line: 12, character: 4 });
+        expect(usageEventFor({ type: 'ready' }, now)).toBeNull();
+        expect(usageEventFor({ type: 'highlight', range: null }, now)).toBeNull();
+        expect(usageEventFor({ type: 'usage' }, now)).toBeNull();
+    });
+});

client/src/utils/usage-log.ts

@@ -0,0 +1,48 @@
+/**
+ * The usage log (liquidjava.usageLog): one JSON line per use of the LiquidJava view, for user studies.
+ * This module is the pure part, so it can be tested without VS Code; services/usage-log.ts writes the file.
+ */
+
+/** A message the webview posts when something in the view is used */
+export interface UsageMessage {
+    type: "usage";
+    /** what was used: tab, hints, found-step, state-machine, state-error-step, reveal, context, context-section, copy, scope, diagram */
+    action: string;
+    [detail: string]: unknown;
+}
+
+/** What one line of the log holds */
+export interface UsageEvent {
+    t: string;
+    event: string;
+    [detail: string]: unknown;
+}
+
+export function isUsageMessage(message: unknown): message is UsageMessage {
+    return typeof message === "object" && message !== null
+        && (message as { type?: unknown }).type === "usage"
+        && typeof (message as { action?: unknown }).action === "string";
+}
+
+/**
+ * The log line for a message from the webview, or null for messages that are not uses of the view.
+ * An openFile message (a click on a location in the view) is logged as `location`
+ * @param message what the webview posted
+ * @param now the time of the event
+ */
+export function usageEventFor(message: unknown, now: Date = new Date()): UsageEvent | null {
+    if (isUsageMessage(message)) {
+        const { type: _type, action, ...detail } = message;
+        return { t: now.toISOString(), event: action, ...detail };
+    }
+    if (typeof message === "object" && message !== null && (message as { type?: unknown }).type === "openFile") {
+        const { filePath, line, character } = message as { filePath?: unknown; line?: unknown; character?: unknown };
+        return { t: now.toISOString(), event: "location", file: filePath, line, character };
+    }
+    return null;
+}
+
+/** The line appended to the file: JSON and a newline */
+export function formatUsageLine(event: UsageEvent): string {
+    return JSON.stringify(event) + "\n";
+}

client/src/webview/script.spec.ts

@@ -141,6 +141,30 @@ describe('webview script', () => {
         expect(root.querySelector('.info')?.textContent).toContain('Running the LiquidJava verification');
     });
 
+    it('posts a usage message for a tab switch and for the hints toggle (liquidjava.usageLog)', () => {
+        showDiagnostics([{ ...diagnostic(currentFile, 'State error'), hints: [{ kind: 'general', message: 'Call `open()` first' }] }]);
+        receive({ type: 'context', context: context() });
+        postMessage.mockClear();
+
+        click('[data-tab="context"]');
+        expect(postMessage.mock.calls).toContainEqual([{ type: 'usage', action: 'tab', tab: 'context' }]);
+
+        click('[data-tab="diagnostics"]');
+        postMessage.mockClear();
+        const details = root.querySelector<HTMLDetailsElement>('details[data-hint-key]');
+        expect(details, 'the hints are rendered closed').not.toBeNull();
+        expect(details!.open).toBe(false);
+        // a toggle without a click or key on the summary is a render (an open hint drawn again), not a use
+        details!.open = true;
+        details!.dispatchEvent(new dom.window.Event('toggle'));
+        expect(postMessage.mock.calls.filter(([m]) => (m as { action?: string }).action === 'hints')).toEqual([]);
+        details!.open = false;
+        click('details[data-hint-key] > summary');
+        details!.open = true;
+        details!.dispatchEvent(new dom.window.Event('toggle'));
+        expect(postMessage.mock.calls).toContainEqual([{ type: 'usage', action: 'hints', open: true, error: details!.getAttribute('data-hint-key') }]);
+    });
+
     it('switches between diagnostics, context, and state machine tabs', async () => {
         showDiagnostics([diagnostic(currentFile, 'Current error')]);
         receive({ type: 'context', context: context() });
@@ -168,8 +192,11 @@ describe('webview script', () => {
         expect(root.querySelector('.diagram-container')).toBeNull();
         expect(postMessage.mock.calls).toEqual([
             [{ type: 'highlight', range: null }],
+            [{ type: 'usage', action: 'tab', tab: 'context' }],
             [{ type: 'highlight', range: null }],
+            [{ type: 'usage', action: 'tab', tab: 'fsm' }],
             [{ type: 'highlight', range: null }],
+            [{ type: 'usage', action: 'tab', tab: 'diagnostics' }],
         ]);
     });