From b50c56755037bb062cf0be7a8361c904674813e2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Mon, 26 Oct 2026 12:17:38 +0100 Subject: [PATCH 1/2] Put the error actions on the title line and collapse hints (#164) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Description Stacked on #161; merge that first. - **Actions on the title line.** **Show in state machine** now 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.** A hint is a `Hint` section the user can open. A hint the user opens stays open after a new verification, so editing the code does not close it. Hints are matched across verifications by the diagnostic's position, the same key the state errors already use, now shared as `getDiagnosticKey`. ## Screenshots `E_OSS_A1_17_InterruptManager` from the C-stars proposal in building-examples-liquidjava. **Before** Error card with Show in state machine below the title and the hint open **After**, with the hint closed and then opened. Error card with Show in state machine on the title line and a closed hint Error card with the hint opened **A narrow side bar**: the actions wrap below the title. Narrow side bar with the actions below the title ## Tests - `npm run lint` and `npm run test:typecheck`: clean. - `npm run test:unit`: 95 passed. In `script.spec.ts`, the state machine button test now checks that it is the first action on the title line, and a new test checks that hints start closed and stay open or closed after a new verification. - `npm test` (VS Code): 9 + 1 passing. Server `mvn test` and the local smoke test: passed. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 --- client/src/webview/diagnostic-reveal.ts | 9 +++++ client/src/webview/script.spec.ts | 27 ++++++++++++--- client/src/webview/script.ts | 9 ++++- client/src/webview/state-errors.ts | 6 ++-- client/src/webview/styles.ts | 25 +++++++++++--- .../src/webview/views/diagnostics/errors.ts | 17 +++++----- .../src/webview/views/diagnostics/warnings.ts | 12 +++---- client/src/webview/views/sections.ts | 34 ++++++++++++++++--- 8 files changed, 106 insertions(+), 33 deletions(-) diff --git a/client/src/webview/diagnostic-reveal.ts b/client/src/webview/diagnostic-reveal.ts index 2a95ef6e..cb8bcacd 100644 --- a/client/src/webview/diagnostic-reveal.ts +++ b/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}`; +} diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index 9b814ef3..b6fdd550 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -402,10 +402,29 @@ 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('keeps hints closed until opened, and open after a new verification', () => { + const error = { ...stateError('State refinement error', errorMachine('Counter', 'close')), hint: 'Call open() first' }; + showDiagnostics([error]); + const hint = () => root.querySelector('.error-item .hint-section')!; + expect(hint().open).toBe(false); + expect(hint().querySelector('summary')?.textContent).toBe('Hint'); + expect(hint().querySelector('pre')?.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', () => { diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 672795e5..cc44922d 100644 --- a/client/src/webview/script.ts +++ b/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; diff --git a/client/src/webview/state-errors.ts b/client/src/webview/state-errors.ts index 88e7a194..52a96a89 100644 --- a/client/src/webview/state-errors.ts +++ b/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); } /** diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index abef3e0e..0a893f5a 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -195,12 +195,28 @@ 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; } .copy-diagnostic-btn, .diagnostic-context-btn { @@ -252,8 +268,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; diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index 1b9db342..f3d2536d 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -14,6 +14,7 @@ import type { SyntaxError, } from "../../../types/diagnostics"; import { renderCopyDiagnosticButton } from "./diagnostics"; +import { getDiagnosticKey } from "../../diagnostic-reveal"; export function renderErrors(errors: LJError[]): string { return /*html*/` @@ -21,11 +22,11 @@ export function renderErrors(errors: LJError[]): string { ${errors.map((error, index) => { return /*html*/`
  • -
    + ${renderError(error, /*html*/` + ${renderDiagnosticStateMachineAction(error, index)} ${renderDiagnosticContextAction(error)} ${renderCopyDiagnosticButton('error', index)} -
    - ${renderError(error, renderDiagnosticStateMachineAction(error, index))} + `)}
    • `; }).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 = renderHint(error.hint, getDiagnosticKey(error)); const location = renderLocation(error); - return /*html*/`${header}${headerActions}${content}${hint}${location}`; + return /*html*/`${header}${content}${hint}${location}`; } function renderDiagnosticContextAction(error: LJError): string { diff --git a/client/src/webview/views/diagnostics/warnings.ts b/client/src/webview/views/diagnostics/warnings.ts index 82f41b0b..47de9d2a 100644 --- a/client/src/webview/views/diagnostics/warnings.ts +++ b/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 { renderCopyDiagnosticButton } from "./diagnostics"; +import { getDiagnosticKey } from "../../diagnostic-reveal"; export function renderWarnings(warnings: LJWarning[]): string { return /*html*/` @@ -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 = renderHint(warning.hint, getDiagnosticKey(warning)); const location = renderLocation(warning); return /*html*/`${header}${content}${hint}${location}`; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 3dd7b6d3..e72f3ef8 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -21,8 +21,29 @@ export const renderSection = (title: string, body: string): string => /*html*/ export const renderExpressionSection = (title: string, expression: string): string => /*html*/ renderCustomSection(title, renderHighlightedExpression(expression)); -export const renderHint = (hint: string | null): string => - hint?.trim() ? renderCustomSection('Hint', `
    ${escapeHtml(hint.trim())}
    `) : ''; +// hints the user opened, kept open when the diagnostics are rendered again +const openHints = new Set(); + +export function setHintOpen(key: string, open: boolean) { + if (open) openHints.add(key); + else openHints.delete(key); +} + +/** + * Renders the hint of a diagnostic, closed until the user opens it + * @param hint The hint text + * @param key Identifies the diagnostic, so an opened hint stays open after a new verification + */ +export function renderHint(hint: string | null, key?: string): string { + if (!hint?.trim()) return ''; + const open = key !== undefined && openHints.has(key); + return /*html*/` +
    + Hint + 
    ${escapeHtml(hint.trim())}
    +
    + `; +} export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/` `; -export const renderDiagnosticHeader = (title: string, message: string): string => /*html*/ - `

    ${title}

    ${message}

    `; +export const renderDiagnosticHeader = (title: string, message: string, actions = ''): string => /*html*/` +
    +

    ${title}

    + ${actions.trim() ? `
    ${actions}
    ` : ''} +
    +

    ${message}

    +`; export function renderDiagnosticDataAttributes(diagnostic: LJDiagnostic): string { const target = getDiagnosticRevealTarget(diagnostic); From 53c360fd6783f83f2f110f43b0f274c0e1fcee0c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 26 Oct 2026 11:39:45 +0000 Subject: [PATCH 2/2] Send the hints as a list and show call sequences as separate options The server sends each hint with its kind instead of one joined string. When the verifier suggests several call sequences, the view lists them as alternatives under Any one of these, apart from the hints that explain the error. Co-Authored-By: Claude Opus 5.5 --- client/src/types/diagnostics.ts | 11 ++++- client/src/webview/script.spec.ts | 42 +++++++++++++++++-- client/src/webview/state-errors.spec.ts | 2 +- client/src/webview/styles.ts | 30 +++++++++++++ .../views/diagnostics/diagnostics.spec.ts | 4 +- .../src/webview/views/diagnostics/errors.ts | 4 +- .../src/webview/views/diagnostics/warnings.ts | 4 +- client/src/webview/views/sections.ts | 33 +++++++++++---- .../main/java/dtos/diagnostics/HintDTO.java | 24 +++++++++++ .../dtos/diagnostics/LJDiagnosticDTO.java | 10 +++-- .../src/main/java/dtos/errors/LJErrorDTO.java | 7 +++- .../java/utils/DiagnosticConverterTest.java | 18 +++++++- 12 files changed, 161 insertions(+), 28 deletions(-) create mode 100644 server/src/main/java/dtos/diagnostics/HintDTO.java diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 9cc7f1f8..2c03de4c 100644 --- a/client/src/types/diagnostics.ts +++ b/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; } diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index b6fdd550..c7c1219b 100644 --- a/client/src/webview/script.spec.ts +++ b/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, @@ -408,13 +408,47 @@ describe('webview script', () => { 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')), hint: 'Call open() first' }; + const error = { ...stateError('State refinement error', errorMachine('Counter', 'close')), hints: [{ kind: 'general' as const, message: 'Call open() first' }] }; showDiagnostics([error]); const hint = () => root.querySelector('.error-item .hint-section')!; expect(hint().open).toBe(false); expect(hint().querySelector('summary')?.textContent).toBe('Hint'); - expect(hint().querySelector('pre')?.textContent).toBe('Call open() first'); + expect(hint().querySelector('.hint-message')?.textContent).toBe('Call open() first'); hint().open = true; hint().dispatchEvent(new Event('toggle')); diff --git a/client/src/webview/state-errors.spec.ts b/client/src/webview/state-errors.spec.ts index 0c7c41fe..b93de4a5 100644 --- a/client/src/webview/state-errors.spec.ts +++ b/client/src/webview/state-errors.spec.ts @@ -20,7 +20,7 @@ function stateError(line: number, overrides: Partial = {}) 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 }, diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 0a893f5a..be36de7d 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -218,6 +218,36 @@ export function getStyles(): string { .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 { display: inline-flex; diff --git a/client/src/webview/views/diagnostics/diagnostics.spec.ts b/client/src/webview/views/diagnostics/diagnostics.spec.ts index 5b58a51c..8d9d430c 100644 --- a/client/src/webview/views/diagnostics/diagnostics.spec.ts +++ b/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, }; } diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index f3d2536d..d79c611d 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/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 { @@ -76,7 +76,7 @@ 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 || '', actions); const content = (errorContentRenderers[error.type] as (error: LJError) => string)?.(error) || ''; - const hint = renderHint(error.hint, getDiagnosticKey(error)); + const hint = renderHints(error.hints, getDiagnosticKey(error)); const location = renderLocation(error); return /*html*/`${header}${content}${hint}${location}`; } diff --git a/client/src/webview/views/diagnostics/warnings.ts b/client/src/webview/views/diagnostics/warnings.ts index 47de9d2a..e718bc55 100644 --- a/client/src/webview/views/diagnostics/warnings.ts +++ b/client/src/webview/views/diagnostics/warnings.ts @@ -1,5 +1,5 @@ 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"; @@ -34,7 +34,7 @@ const warningContentRenderers: WarningContentRenderers = { 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, getDiagnosticKey(warning)); + const hint = renderHints(warning.hints, getDiagnosticKey(warning)); const location = renderLocation(warning); return /*html*/`${header}${content}${hint}${location}`; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index e72f3ef8..bc1d02f3 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -1,4 +1,4 @@ -import type { LJDiagnostic, SourcePosition } from "../../types/diagnostics"; +import type { LJDiagnostic, LJHint, SourcePosition } from "../../types/diagnostics"; import { escapeHtml, getFileName, getSimpleName } from "../utils"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../highlighting"; import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal"; @@ -30,21 +30,38 @@ export function setHintOpen(key: string, open: boolean) { } /** - * Renders the hint of a diagnostic, closed until the user opens it - * @param hint The hint text - * @param key Identifies the diagnostic, so an opened hint stays open after a new verification + * Renders the hints of a diagnostic, closed until the user opens them + * Several call sequences are alternatives, so they are listed as options apart from the hints that explain the error + * @param hints The hints of the diagnostic + * @param key Identifies the diagnostic, so opened hints stay open after a new verification */ -export function renderHint(hint: string | null, key?: string): string { - if (!hint?.trim()) return ''; +export function renderHints(hints: LJHint[] | undefined, key?: string): string { + const shown = (hints ?? []).filter(hint => hint.message.trim()); + if (shown.length === 0) return ''; + const options = shown.filter(hint => hint.kind === 'call-sequence'); + const listsOptions = options.length > 1; + const notes = listsOptions ? shown.filter(hint => hint.kind !== 'call-sequence') : shown; const open = key !== undefined && openHints.has(key); return /*html*/`
    - Hint - 
    ${escapeHtml(hint.trim())}
    + ${shown.length === 1 ? 'Hint' : 'Hints'} +
    + ${listsOptions ? /*html*/` +
    +

    Any one of these:

    +
      ${options.map(hint => `
    • ${renderHintMessage(hint)}
      • `).join('')}
    +
    + ` : ''} + ${notes.map(hint => `
    ${renderHintMessage(hint)}
    `).join('')} +
    `; } +function renderHintMessage(hint: LJHint): string { + return `${escapeHtml(hint.message.trim())}`; +} + export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/`