diff --git a/client/src/webview/diagnostic-reveal.ts b/client/src/webview/diagnostic-reveal.ts index 2a95ef6..cb8bcac 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 9b814ef..b6fdd55 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 672795e..cc44922 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 88e7a19..52a96a8 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 abef3e0..0a893f5 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 1b9db34..f3d2536 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 82f41b0..47de9d2 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 3dd7b6d..e72f3ef 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);