From ec7edf97bccc0ce9905def186b86b8f8a9606946 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 26 Oct 2026 10:59:46 +0000 Subject: [PATCH] Put the error actions on the title line and collapse hints Show in state machine sits on the line of the error title with the other actions, and hints start closed. A hint the user opens stays open after a new verification. 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*/`
      ${warnings.map((warning, index) => /*html*/`
    • -
      - ${renderCopyDiagnosticButton('warning', index)} -
      - ${renderWarning(warning)} + ${renderWarning(warning, renderCopyDiagnosticButton('warning', index))}
      • `).join("")}
    @@ -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);