Put the error actions on the title line, collapse hints, and show hints as separate options

client/src/types/diagnostics.ts

@@ -23,10 +23,19 @@ export type LJError = CustomError | IllegalConstructorTransitionError |
 
 export type LJWarning = CustomWarning | ExternalClassNotFoundWarning | ExternalMethodNotFoundWarning | UnsatisfiableRefinementWarning;
 
+// what a hint is about, as the verifier names it, e.g. 'call-sequence' for calls that bring the object to a state that allows the failing call
+export type LJHintKind = 'general' | 'deciding-argument' | 'call-sequence' | 'available-calls' | 'unreachable-state'
+    | 'path-dependent-state' | 'final-state' | 'reaching-calls';
+
+export type LJHint = {
+    kind: LJHintKind;
+    message: string;
+};
+
 type BaseDiagnostic = {
     title: string;
     message: string;
-    hint: string | null;
+    hints: LJHint[];
     file: string;
     position: SourcePosition | null;
 }

client/src/webview/diagnostic-reveal.ts

@@ -29,3 +29,12 @@ export function getDiagnosticRevealTargetFromKey(value?: string | null): Diagnos
         }
     };
 }
+
+/**
+ * Gets a key that identifies a diagnostic across verifications
+ * This is its reveal key, or, without a position, its file, title, and message, which never match the reveal key pattern
+ */
+export function getDiagnosticKey(diagnostic: LJDiagnostic): string {
+    const target = getDiagnosticRevealTarget(diagnostic);
+    return target ? getDiagnosticRevealTargetKey(target) : `${diagnostic.file}#${diagnostic.title}#${diagnostic.message}`;
+}

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`,
-        hint: null,
+        hints: [],
         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`, hint: null, file, position: errorPosition,
+        title, message: `${title} message`, hints: [], 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, stateMachine: sm,
@@ -402,10 +402,63 @@ describe('webview script', () => {
         showDiagnostics([stateError('State refinement error', errorMachine('Counter', 'close'))]);
 
         expect(root.querySelector('.diagnostic-state-machine-btn')?.textContent?.trim()).toBe('Show in state machine');
-        expect(root.querySelector('.diagnostic-actions .diagnostic-state-machine-btn')).toBeNull();
-        // right below the error message, before its details
-        const firstSection = root.querySelector('.error-item .section')!;
-        expect(root.querySelector('.diagnostic-state-machine-btn')!.compareDocumentPosition(firstSection)).toBe(Node.DOCUMENT_POSITION_FOLLOWING);
+        // on the line of the title, before the other actions
+        const actions = root.querySelector('.error-item .diagnostic-title-row .diagnostic-actions')!;
+        expect(actions.firstElementChild?.classList.contains('diagnostic-state-machine-btn')).toBe(true);
+        expect(actions.querySelector('.copy-diagnostic-btn')).not.toBeNull();
+    });
+
+    it('lists several call sequences as separate options, apart from the other hints', () => {
+        showDiagnostics([{
+            ...stateError('State refinement error', errorMachine('Counter', 'close')),
+            hints: [
+                { kind: 'call-sequence', message: 'Call counter.open() before this call to move counter from Closed to Open' },
+                { kind: 'call-sequence', message: 'Call counter.reset() before this call to move counter from Closed to Open' },
+                { kind: 'available-calls', message: 'In state Closed, counter can call: open(), reset()' },
+            ],
+        }]);
+        const hints = root.querySelector('.error-item .hint-section')!;
+
+        expect(hints.querySelector('summary')?.textContent).toBe('Hints');
+        expect(hints.querySelector('.hint-options-title')?.textContent).toBe('Any one of these:');
+        expect(Array.from(hints.querySelectorAll('.hint-options li'), item => item.textContent)).toEqual([
+            'Call counter.open() before this call to move counter from Closed to Open',
+            'Call counter.reset() before this call to move counter from Closed to Open',
+        ]);
+        expect(Array.from(hints.querySelectorAll('.hint-note'), note => note.textContent)).toEqual(['In state Closed, counter can call: open(), reset()']);
+    });
+
+    it('shows a single call sequence as a hint, not as a list of options', () => {
+        showDiagnostics([{
+            ...stateError('State refinement error', errorMachine('Counter', 'close')),
+            hints: [
+                { kind: 'call-sequence', message: 'Call counter.open() before this call to move counter from Closed to Open' },
+                { kind: 'available-calls', message: 'In state Closed, counter can call: open()' },
+            ],
+        }]);
+        const hints = root.querySelector('.error-item .hint-section')!;
+
+        expect(hints.querySelector('.hint-options')).toBeNull();
+        expect(hints.querySelectorAll('.hint-note')).toHaveLength(2);
+    });
+
+    it('keeps hints closed until opened, and open after a new verification', () => {
+        const error = { ...stateError('State refinement error', errorMachine('Counter', 'close')), hints: [{ kind: 'general' as const, message: 'Call open() first' }] };
+        showDiagnostics([error]);
+        const hint = () => root.querySelector<HTMLDetailsElement>('.error-item .hint-section')!;
+        expect(hint().open).toBe(false);
+        expect(hint().querySelector('summary')?.textContent).toBe('Hint');
+        expect(hint().querySelector('.hint-message')?.textContent).toBe('Call open() first');
+
+        hint().open = true;
+        hint().dispatchEvent(new Event('toggle'));
+        receive({ type: 'diagnostics', diagnostics: [{ ...error }] });
+        expect(hint().open).toBe(true);
+
+        hint().open = false;
+        hint().dispatchEvent(new Event('toggle'));
+        receive({ type: 'diagnostics', diagnostics: [{ ...error }] });
+        expect(hint().open).toBe(false);
     });
 
     it('opens on the first state error of a newly opened file', () => {

client/src/webview/script.ts

@@ -7,7 +7,7 @@ import type { LJDiagnostic, RefinementMismatchError, StateRefinementError } from
 import type { Range } from "../types/context";
 import type { LJStateMachine } from "../types/fsm";
 import type { ExtensionStatus } from "../state";
-import type { NavTab } from "./views/sections";
+import { setHintOpen, type NavTab } from "./views/sections";
 import { copyDiagnosticToClipboard, getDisplayDiagnostics, renderDiagnosticsView } from "./views/diagnostics/diagnostics";
 import type { LJContext } from "../types/context";
 import { ContextSectionState, renderContextView } from "./views/context/context";
@@ -56,6 +56,13 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
     vscode.postMessage({ type: 'ready' });    
 
     // on click
+    // toggle does not bubble, so it is caught on its way down
+    root.addEventListener('toggle', (e: Event) => {
+        const details = e.target as HTMLDetailsElement;
+        const key = details.getAttribute?.('data-hint-key');
+        if (key !== null && key !== undefined) setHintOpen(key, details.open);
+    }, true);
+
     root.addEventListener('click', (e: MouseEvent) => {
         const target = e.target instanceof Element ? e.target : null;
         if (!target) return;

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¹⁸)', hint: null,
+        message: 'found childrenAllowed(root¹⁸) but expected maybeHasChildren(root¹⁸)', hints: [],
         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/state-errors.ts

@@ -1,5 +1,5 @@
 import type { LJDiagnostic, StateRefinementError } from "../types/diagnostics";
-import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "./diagnostic-reveal";
+import { getDiagnosticKey, getDiagnosticRevealTargetKey } from "./diagnostic-reveal";
 
 /**
  * Gets the state errors reported in the current file, in source order
@@ -28,9 +28,7 @@ export function getAllStateErrors(diagnostics: LJDiagnostic[] | undefined): Stat
 }
 
 export function getStateErrorKey(error: StateRefinementError): string {
-    const target = getDiagnosticRevealTarget(error);
-    // errors without a position never match the position pattern of reveal keys
-    return target ? getDiagnosticRevealTargetKey(target) : `${error.file}#${error.title}#${error.message}`;
+    return getDiagnosticKey(error);
 }
 
 /**

client/src/webview/styles.ts

@@ -195,12 +195,58 @@ export function getStyles(): string {
             line-height: 1;
             pointer-events: none;
         }
+        .diagnostic-title-row {
+            display: flex;
+            flex-wrap: wrap;
+            align-items: center;
+            justify-content: space-between;
+            gap: 0.25rem 0.75rem;
+        }
+        .diagnostic-title-row h3 {
+            min-width: 0;
+        }
         .diagnostic-actions {
-            position: absolute;
-            top: 0.5rem;
-            right: 0.5rem;
             display: flex;
+            align-items: center;
             gap: 0.25rem;
+            margin-left: auto;
+        }
+        .hint-summary {
+            font-weight: bold;
+            cursor: pointer;
+        }
+        .hint-section[open] .hint-summary {
+            margin-bottom: 0.25rem;
+        }
+        .hint-body {
+            padding: 0.5rem;
+            background-color: var(--vscode-editor-background);
+            border-radius: 4px;
+            font-family: var(--vscode-editor-font-family, monospace);
+            font-size: var(--vscode-editor-font-size, inherit);
+        }
+        .hint-message {
+            white-space: pre-wrap;
+            overflow-wrap: anywhere;
+        }
+        .hint-options-title {
+            margin: 0 0 0.25rem;
+        }
+        .hint-options ul {
+            margin: 0;
+            padding-left: 1.25rem;
+            list-style: disc;
+        }
+        .hint-options li {
+            display: list-item;
+        }
+        .hint-options li + li {
+            margin-top: 0.4rem;
+        }
+        .hint-body > * + * {
+            margin-top: 0.5rem;
+            padding-top: 0.5rem;
+            border-top: 1px solid var(--vscode-panel-border, transparent);
         }
         .copy-diagnostic-btn,
         .diagnostic-context-btn {
@@ -252,8 +298,7 @@ export function getStyles(): string {
             display: inline-flex;
             align-items: center;
             gap: 0.4rem;
-            margin: 0 0 1rem;
-            padding: 0.25rem 0.6rem;
+            padding: 0.15rem 0.5rem;
             color: var(--vscode-button-secondaryForeground);
             background-color: var(--vscode-button-secondaryBackground);
             font-size: 0.85rem;

client/src/webview/views/diagnostics/diagnostics.spec.ts

@@ -8,14 +8,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.', hint: null, file, position: null,
+        message: 'The refinement does not hold.', hints: [], file, position: null,
     };
 }
 
 function warning(file = currentFile): CustomWarning {
     return {
         category: 'warning', type: 'custom-warning', title: 'Verification warning',
-        message: 'Some code could not be verified.', hint: null, file, position: null,
+        message: 'Some code could not be verified.', hints: [], file, position: null,
     };
 }
 

client/src/webview/views/diagnostics/errors.ts

@@ -1,4 +1,4 @@
-import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton, renderHint } from "../sections";
+import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton, renderHints } from "../sections";
 import { renderCounterexample } from "./counterexample";
 import { renderVCImplication } from "./vc-implications";
 import type {
@@ -14,18 +14,19 @@ import type {
     SyntaxError,
 } from "../../../types/diagnostics";
 import { renderCopyDiagnosticButton } from "./diagnostics";
+import { getDiagnosticKey } from "../../diagnostic-reveal";
 
 export function renderErrors(errors: LJError[]): string {
     return /*html*/`
         <ul>
             ${errors.map((error, index) => {
                 return /*html*/`
                 <li class="diagnostic-item error-item" ${renderDiagnosticDataAttributes(error)}>
-                    <div class="diagnostic-actions">
+                    ${renderError(error, /*html*/`
+                        ${renderDiagnosticStateMachineAction(error, index)}
                         ${renderDiagnosticContextAction(error)}
                         ${renderCopyDiagnosticButton('error', index)}
-                    </div>
-                    ${renderError(error, renderDiagnosticStateMachineAction(error, index))}
+                    `)}
                 </li>
             `;
             }).join("")}
@@ -69,15 +70,15 @@ const errorContentRenderers: ErrorRendererMap = {
 /**
  * Renders the error content
  * @param error The error to render
- * @param headerActions Actions shown below the error message
+ * @param actions Actions shown on the line of the error title
  */
-export function renderError(error: LJError, headerActions = ''): string {
+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 || '');
+    const header = renderDiagnosticHeader(error.title, message || '', actions);
     const content = (errorContentRenderers[error.type] as (error: LJError) => string)?.(error) || '';
-    const hint = renderHint(error.hint);
+    const hint = renderHints(error.hints, getDiagnosticKey(error));
     const location = renderLocation(error);
-    return /*html*/`${header}${headerActions}${content}${hint}${location}`;
+    return /*html*/`${header}${content}${hint}${location}`;
 }
 
 function renderDiagnosticContextAction(error: LJError): string {

client/src/webview/views/diagnostics/warnings.ts

@@ -1,16 +1,14 @@
 import type { CustomWarning, ExternalClassNotFoundWarning, ExternalMethodNotFoundWarning, LJWarning, UnsatisfiableRefinementWarning } from "../../../types/diagnostics";
-import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderHint, renderLocation } from "../sections";
+import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderHints, renderLocation } from "../sections";
 import { renderCopyDiagnosticButton } from "./diagnostics";
+import { getDiagnosticKey } from "../../diagnostic-reveal";
 
 export function renderWarnings(warnings: LJWarning[]): string {
     return /*html*/`
         <ul>
                 ${warnings.map((warning, index) => /*html*/`
                 <li class="diagnostic-item warning-item" ${renderDiagnosticDataAttributes(warning)}>
-                    <div class="diagnostic-actions">
-                        ${renderCopyDiagnosticButton('warning', index)}
-                    </div>
-                    ${renderWarning(warning)}
+                    ${renderWarning(warning, renderCopyDiagnosticButton('warning', index))}
                 </li>
             `).join("")}
         </ul>    
@@ -33,10 +31,10 @@ const warningContentRenderers: WarningContentRenderers = {
     "custom-warning": (_: CustomWarning) => ""
 };
 
-export function renderWarning(warning: LJWarning): string {
-    const header = renderDiagnosticHeader(warning.title, warning.message);
+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 = renderHint(warning.hint);
+    const hint = renderHints(warning.hints, getDiagnosticKey(warning));
     const location = renderLocation(warning);
     return /*html*/`${header}${content}${hint}${location}`;
 }