Skip to content

Commit a4cbd80

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
authored
Put the error actions on the title line, collapse hints, and show hints as separate options (#165)
## Description Replaces #164, which was merged into the #161 branch after #161 had been merged into main, so it never reached main. The first commit is #164 unchanged; the second separates the hints. **Error title line (from #164).** **Show in state machine** sits on the line of the error title, before the View related context and copy icons. When the side bar is too narrow, the actions wrap below the title, aligned right. Warnings get the same title line for their copy icon. **Hints start closed (from #164).** The hints are a `Hint` / `Hints` section the user can open. Hints the user opens stay open after a new verification, so editing does not close them. **Separate hints.** The verifier reports a list of hints, each with a kind, but the server joined them into one string, so several suggested call sequences read as if all of them had to be applied. - **Server:** `hints` is now a list of `{ kind, message }`, from `LJDiagnostic#getHints()`, replacing the joined `hint` string. The kind is the verifier's `Hint.Kind` in kebab case, e.g. `call-sequence`. - **View:** two or more `call-sequence` hints are listed as bullets under **Any one of these:**. Every other hint, such as the calls available in the current state, is its own paragraph, separated by a line. A single call sequence is shown as a plain hint. ## Screenshots `E_OSS_A1_17_InterruptManager` from the C-stars proposal in building-examples-liquidjava, where the verifier suggests three call sequences and lists the available calls. **Before:** the action below the title, and the three call sequences and the available calls run together. <img width="560" alt="Error card before: Show in state machine below the title" src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/before-card.png" /> <img width="560" alt="Hints before: all suggestions run together" src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/before-hints.png" /> **After:** the actions on the title line, the hints closed and then opened. <img width="560" alt="Error card with the actions on the title line and the hints closed" src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/after-closed.png" /> <img width="560" alt="Hints opened: Any one of these with three bullets, then the available calls" src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/after-open.png" /> **A narrow side bar:** the actions wrap below the title. <img width="360" alt="Narrow side bar with the actions below the title" src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/hint-list/after-narrow.png" /> ## Tests - Server `mvn test`: 28 passing. New `DiagnosticConverterTest` test: each hint keeps its kind and message, in order. - `npm run lint` and `npm run test:typecheck`: clean. - `npm run test:unit`: 97 passed. New tests in `script.spec.ts`: - hints start closed and stay open or closed after a new verification; - several call sequences are listed as options apart from the other hints; - a single call sequence is a plain hint; - the state machine button is the first action on the title line. - `npm test` (VS Code): 9 + 1 passing. Local smoke test: passed. After the full run I only changed the CSS of the option list (bullets and spacing). Unit tests and lint were re-run after it. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 7b6a3bd commit a4cbd80

15 files changed

Lines changed: 256 additions & 50 deletions

File tree

‎client/src/types/diagnostics.ts‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,10 +23,19 @@ export type LJError = CustomError | IllegalConstructorTransitionError |
2323

2424
export type LJWarning = CustomWarning | ExternalClassNotFoundWarning | ExternalMethodNotFoundWarning | UnsatisfiableRefinementWarning;
2525

26+
// 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
27+
export type LJHintKind = 'general' | 'deciding-argument' | 'call-sequence' | 'available-calls' | 'unreachable-state'
28+
| 'path-dependent-state' | 'final-state' | 'reaching-calls';
29+
30+
export type LJHint = {
31+
kind: LJHintKind;
32+
message: string;
33+
};
34+
2635
type BaseDiagnostic = {
2736
title: string;
2837
message: string;
29-
hint: string | null;
38+
hints: LJHint[];
3039
file: string;
3140
position: SourcePosition | null;
3241
}

‎client/src/webview/diagnostic-reveal.ts‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,12 @@ export function getDiagnosticRevealTargetFromKey(value?: string | null): Diagnos
2929
}
3030
};
3131
}
32+
33+
/**
34+
* Gets a key that identifies a diagnostic across verifications
35+
* This is its reveal key, or, without a position, its file, title, and message, which never match the reveal key pattern
36+
*/
37+
export function getDiagnosticKey(diagnostic: LJDiagnostic): string {
38+
const target = getDiagnosticRevealTarget(diagnostic);
39+
return target ? getDiagnosticRevealTargetKey(target) : `${diagnostic.file}#${diagnostic.title}#${diagnostic.message}`;
40+
}

‎client/src/webview/script.spec.ts‎

Lines changed: 59 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ function diagnostic(file: string, title: string, category: 'error' | 'warning' =
1818
const details = {
1919
title,
2020
message: `${title} message`,
21-
hint: null,
21+
hints: [],
2222
file,
2323
position: { ...position, file },
2424
};
@@ -60,7 +60,7 @@ const stateMachine: LJStateMachine = {
6060
function stateError(title: string, sm: LJStateMachine, line = position.lineStart, file = currentFile): LJDiagnostic {
6161
const errorPosition = { ...position, file, lineStart: line, lineEnd: line };
6262
return {
63-
title, message: `${title} message`, hint: null, file, position: errorPosition,
63+
title, message: `${title} message`, hints: [], file, position: errorPosition,
6464
category: 'error', type: 'state-refinement-error', translationTable: {}, expected: 'Open(counter)',
6565
found: { implication: null as never, origin: null, simplification: 'Closed(counter)' },
6666
customMessage: '', declarationPosition: null, stateMachine: sm,
@@ -402,10 +402,63 @@ describe('webview script', () => {
402402
showDiagnostics([stateError('State refinement error', errorMachine('Counter', 'close'))]);
403403

404404
expect(root.querySelector('.diagnostic-state-machine-btn')?.textContent?.trim()).toBe('Show in state machine');
405-
expect(root.querySelector('.diagnostic-actions .diagnostic-state-machine-btn')).toBeNull();
406-
// right below the error message, before its details
407-
const firstSection = root.querySelector('.error-item .section')!;
408-
expect(root.querySelector('.diagnostic-state-machine-btn')!.compareDocumentPosition(firstSection)).toBe(Node.DOCUMENT_POSITION_FOLLOWING);
405+
// on the line of the title, before the other actions
406+
const actions = root.querySelector('.error-item .diagnostic-title-row .diagnostic-actions')!;
407+
expect(actions.firstElementChild?.classList.contains('diagnostic-state-machine-btn')).toBe(true);
408+
expect(actions.querySelector('.copy-diagnostic-btn')).not.toBeNull();
409+
});
410+
411+
it('lists several call sequences as separate options, apart from the other hints', () => {
412+
showDiagnostics([{
413+
...stateError('State refinement error', errorMachine('Counter', 'close')),
414+
hints: [
415+
{ kind: 'call-sequence', message: 'Call counter.open() before this call to move counter from Closed to Open' },
416+
{ kind: 'call-sequence', message: 'Call counter.reset() before this call to move counter from Closed to Open' },
417+
{ kind: 'available-calls', message: 'In state Closed, counter can call: open(), reset()' },
418+
],
419+
}]);
420+
const hints = root.querySelector('.error-item .hint-section')!;
421+
422+
expect(hints.querySelector('summary')?.textContent).toBe('Hints');
423+
expect(hints.querySelector('.hint-options-title')?.textContent).toBe('Any one of these:');
424+
expect(Array.from(hints.querySelectorAll('.hint-options li'), item => item.textContent)).toEqual([
425+
'Call counter.open() before this call to move counter from Closed to Open',
426+
'Call counter.reset() before this call to move counter from Closed to Open',
427+
]);
428+
expect(Array.from(hints.querySelectorAll('.hint-note'), note => note.textContent)).toEqual(['In state Closed, counter can call: open(), reset()']);
429+
});
430+
431+
it('shows a single call sequence as a hint, not as a list of options', () => {
432+
showDiagnostics([{
433+
...stateError('State refinement error', errorMachine('Counter', 'close')),
434+
hints: [
435+
{ kind: 'call-sequence', message: 'Call counter.open() before this call to move counter from Closed to Open' },
436+
{ kind: 'available-calls', message: 'In state Closed, counter can call: open()' },
437+
],
438+
}]);
439+
const hints = root.querySelector('.error-item .hint-section')!;
440+
441+
expect(hints.querySelector('.hint-options')).toBeNull();
442+
expect(hints.querySelectorAll('.hint-note')).toHaveLength(2);
443+
});
444+
445+
it('keeps hints closed until opened, and open after a new verification', () => {
446+
const error = { ...stateError('State refinement error', errorMachine('Counter', 'close')), hints: [{ kind: 'general' as const, message: 'Call open() first' }] };
447+
showDiagnostics([error]);
448+
const hint = () => root.querySelector<HTMLDetailsElement>('.error-item .hint-section')!;
449+
expect(hint().open).toBe(false);
450+
expect(hint().querySelector('summary')?.textContent).toBe('Hint');
451+
expect(hint().querySelector('.hint-message')?.textContent).toBe('Call open() first');
452+
453+
hint().open = true;
454+
hint().dispatchEvent(new Event('toggle'));
455+
receive({ type: 'diagnostics', diagnostics: [{ ...error }] });
456+
expect(hint().open).toBe(true);
457+
458+
hint().open = false;
459+
hint().dispatchEvent(new Event('toggle'));
460+
receive({ type: 'diagnostics', diagnostics: [{ ...error }] });
461+
expect(hint().open).toBe(false);
409462
});
410463

411464
it('opens on the first state error of a newly opened file', () => {

‎client/src/webview/script.ts‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ import type { LJDiagnostic, RefinementMismatchError, StateRefinementError } from
77
import type { Range } from "../types/context";
88
import type { LJStateMachine } from "../types/fsm";
99
import type { ExtensionStatus } from "../state";
10-
import type { NavTab } from "./views/sections";
10+
import { setHintOpen, type NavTab } from "./views/sections";
1111
import { copyDiagnosticToClipboard, getDisplayDiagnostics, renderDiagnosticsView } from "./views/diagnostics/diagnostics";
1212
import type { LJContext } from "../types/context";
1313
import { ContextSectionState, renderContextView } from "./views/context/context";
@@ -56,6 +56,13 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
5656
vscode.postMessage({ type: 'ready' });
5757

5858
// on click
59+
// toggle does not bubble, so it is caught on its way down
60+
root.addEventListener('toggle', (e: Event) => {
61+
const details = e.target as HTMLDetailsElement;
62+
const key = details.getAttribute?.('data-hint-key');
63+
if (key !== null && key !== undefined) setHintOpen(key, details.open);
64+
}, true);
65+
5966
root.addEventListener('click', (e: MouseEvent) => {
6067
const target = e.target instanceof Element ? e.target : null;
6168
if (!target) return;

‎client/src/webview/state-errors.spec.ts‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ function stateError(line: number, overrides: Partial<StateRefinementError> = {})
2020
const file = overrides.file ?? callerFile;
2121
return {
2222
category: 'error', type: 'state-refinement-error', title: 'State Refinement Error',
23-
message: 'found childrenAllowed(root¹⁸) but expected maybeHasChildren(root¹⁸)', hint: null,
23+
message: 'found childrenAllowed(root¹⁸) but expected maybeHasChildren(root¹⁸)', hints: [],
2424
file, position: { file, lineStart: line, colStart: 15, lineEnd: line, colEnd: 35 },
2525
translationTable: {}, expected: 'maybeHasChildren(root¹⁸)',
2626
found: { implication: null as never, origin: null, simplification: null },

‎client/src/webview/state-errors.ts‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import type { LJDiagnostic, StateRefinementError } from "../types/diagnostics";
2-
import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "./diagnostic-reveal";
2+
import { getDiagnosticKey, getDiagnosticRevealTargetKey } from "./diagnostic-reveal";
33

44
/**
55
* Gets the state errors reported in the current file, in source order
@@ -28,9 +28,7 @@ export function getAllStateErrors(diagnostics: LJDiagnostic[] | undefined): Stat
2828
}
2929

3030
export function getStateErrorKey(error: StateRefinementError): string {
31-
const target = getDiagnosticRevealTarget(error);
32-
// errors without a position never match the position pattern of reveal keys
33-
return target ? getDiagnosticRevealTargetKey(target) : `${error.file}#${error.title}#${error.message}`;
31+
return getDiagnosticKey(error);
3432
}
3533

3634
/**

‎client/src/webview/styles.ts‎

Lines changed: 50 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -195,12 +195,58 @@ export function getStyles(): string {
195195
line-height: 1;
196196
pointer-events: none;
197197
}
198+
.diagnostic-title-row {
199+
display: flex;
200+
flex-wrap: wrap;
201+
align-items: center;
202+
justify-content: space-between;
203+
gap: 0.25rem 0.75rem;
204+
}
205+
.diagnostic-title-row h3 {
206+
min-width: 0;
207+
}
198208
.diagnostic-actions {
199-
position: absolute;
200-
top: 0.5rem;
201-
right: 0.5rem;
202209
display: flex;
210+
align-items: center;
203211
gap: 0.25rem;
212+
margin-left: auto;
213+
}
214+
.hint-summary {
215+
font-weight: bold;
216+
cursor: pointer;
217+
}
218+
.hint-section[open] .hint-summary {
219+
margin-bottom: 0.25rem;
220+
}
221+
.hint-body {
222+
padding: 0.5rem;
223+
background-color: var(--vscode-editor-background);
224+
border-radius: 4px;
225+
font-family: var(--vscode-editor-font-family, monospace);
226+
font-size: var(--vscode-editor-font-size, inherit);
227+
}
228+
.hint-message {
229+
white-space: pre-wrap;
230+
overflow-wrap: anywhere;
231+
}
232+
.hint-options-title {
233+
margin: 0 0 0.25rem;
234+
}
235+
.hint-options ul {
236+
margin: 0;
237+
padding-left: 1.25rem;
238+
list-style: disc;
239+
}
240+
.hint-options li {
241+
display: list-item;
242+
}
243+
.hint-options li + li {
244+
margin-top: 0.4rem;
245+
}
246+
.hint-body > * + * {
247+
margin-top: 0.5rem;
248+
padding-top: 0.5rem;
249+
border-top: 1px solid var(--vscode-panel-border, transparent);
204250
}
205251
.copy-diagnostic-btn,
206252
.diagnostic-context-btn {
@@ -252,8 +298,7 @@ export function getStyles(): string {
252298
display: inline-flex;
253299
align-items: center;
254300
gap: 0.4rem;
255-
margin: 0 0 1rem;
256-
padding: 0.25rem 0.6rem;
301+
padding: 0.15rem 0.5rem;
257302
color: var(--vscode-button-secondaryForeground);
258303
background-color: var(--vscode-button-secondaryBackground);
259304
font-size: 0.85rem;

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,14 +8,14 @@ const otherFile = 'file:///workspace/Other.java';
88
function error(file = currentFile, title = 'Invalid refinement'): CustomError {
99
return {
1010
category: 'error', type: 'custom-error', title,
11-
message: 'The refinement does not hold.', hint: null, file, position: null,
11+
message: 'The refinement does not hold.', hints: [], file, position: null,
1212
};
1313
}
1414

1515
function warning(file = currentFile): CustomWarning {
1616
return {
1717
category: 'warning', type: 'custom-warning', title: 'Verification warning',
18-
message: 'Some code could not be verified.', hint: null, file, position: null,
18+
message: 'Some code could not be verified.', hints: [], file, position: null,
1919
};
2020
}
2121

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

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton, renderHint } from "../sections";
1+
import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton, renderHints } from "../sections";
22
import { renderCounterexample } from "./counterexample";
33
import { renderVCImplication } from "./vc-implications";
44
import type {
@@ -14,18 +14,19 @@ import type {
1414
SyntaxError,
1515
} from "../../../types/diagnostics";
1616
import { renderCopyDiagnosticButton } from "./diagnostics";
17+
import { getDiagnosticKey } from "../../diagnostic-reveal";
1718

1819
export function renderErrors(errors: LJError[]): string {
1920
return /*html*/`
2021
<ul>
2122
${errors.map((error, index) => {
2223
return /*html*/`
2324
<li class="diagnostic-item error-item" ${renderDiagnosticDataAttributes(error)}>
24-
<div class="diagnostic-actions">
25+
${renderError(error, /*html*/`
26+
${renderDiagnosticStateMachineAction(error, index)}
2527
${renderDiagnosticContextAction(error)}
2628
${renderCopyDiagnosticButton('error', index)}
27-
</div>
28-
${renderError(error, renderDiagnosticStateMachineAction(error, index))}
29+
`)}
2930
</li>
3031
`;
3132
}).join("")}
@@ -69,15 +70,15 @@ const errorContentRenderers: ErrorRendererMap = {
6970
/**
7071
* Renders the error content
7172
* @param error The error to render
72-
* @param headerActions Actions shown below the error message
73+
* @param actions Actions shown on the line of the error title
7374
*/
74-
export function renderError(error: LJError, headerActions = ''): string {
75+
export function renderError(error: LJError, actions = ''): string {
7576
const message = error.type === 'refinement-error' || error.type === 'state-refinement-error' ? error.customMessage : error.message;
76-
const header = renderDiagnosticHeader(error.title, message || '');
77+
const header = renderDiagnosticHeader(error.title, message || '', actions);
7778
const content = (errorContentRenderers[error.type] as (error: LJError) => string)?.(error) || '';
78-
const hint = renderHint(error.hint);
79+
const hint = renderHints(error.hints, getDiagnosticKey(error));
7980
const location = renderLocation(error);
80-
return /*html*/`${header}${headerActions}${content}${hint}${location}`;
81+
return /*html*/`${header}${content}${hint}${location}`;
8182
}
8283

8384
function renderDiagnosticContextAction(error: LJError): string {

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

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,14 @@
11
import type { CustomWarning, ExternalClassNotFoundWarning, ExternalMethodNotFoundWarning, LJWarning, UnsatisfiableRefinementWarning } from "../../../types/diagnostics";
2-
import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderHint, renderLocation } from "../sections";
2+
import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderHints, renderLocation } from "../sections";
33
import { renderCopyDiagnosticButton } from "./diagnostics";
4+
import { getDiagnosticKey } from "../../diagnostic-reveal";
45

56
export function renderWarnings(warnings: LJWarning[]): string {
67
return /*html*/`
78
<ul>
89
${warnings.map((warning, index) => /*html*/`
910
<li class="diagnostic-item warning-item" ${renderDiagnosticDataAttributes(warning)}>
10-
<div class="diagnostic-actions">
11-
${renderCopyDiagnosticButton('warning', index)}
12-
</div>
13-
${renderWarning(warning)}
11+
${renderWarning(warning, renderCopyDiagnosticButton('warning', index))}
1412
</li>
1513
`).join("")}
1614
</ul>
@@ -33,10 +31,10 @@ const warningContentRenderers: WarningContentRenderers = {
3331
"custom-warning": (_: CustomWarning) => ""
3432
};
3533

36-
export function renderWarning(warning: LJWarning): string {
37-
const header = renderDiagnosticHeader(warning.title, warning.message);
34+
export function renderWarning(warning: LJWarning, actions = ''): string {
35+
const header = renderDiagnosticHeader(warning.title, warning.message, actions);
3836
const content = (warningContentRenderers[warning.type] as (warning: LJWarning) => string)?.(warning) || '';
39-
const hint = renderHint(warning.hint);
37+
const hint = renderHints(warning.hints, getDiagnosticKey(warning));
4038
const location = renderLocation(warning);
4139
return /*html*/`${header}${content}${hint}${location}`;
4240
}

0 commit comments

Comments
 (0)