Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions client/src/webview/diagnostic-reveal.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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}`;
}
27 changes: 23 additions & 4 deletions client/src/webview/script.spec.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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<HTMLDetailsElement>('.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', () => {
Expand Down
9 changes: 8 additions & 1 deletion client/src/webview/script.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down Expand Up @@ -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;
Expand Down
6 changes: 2 additions & 4 deletions client/src/webview/state-errors.ts
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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);
}

/**
Expand Down
25 changes: 20 additions & 5 deletions client/src/webview/styles.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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;
Expand Down
17 changes: 9 additions & 8 deletions client/src/webview/views/diagnostics/errors.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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("")}
Expand Down Expand Up @@ -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 {
Expand Down
12 changes: 5 additions & 7 deletions client/src/webview/views/diagnostics/warnings.ts
Original file line number Diff line number Diff line change
@@ -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*/`
<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>
Expand All @@ -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}`;
}
34 changes: 30 additions & 4 deletions client/src/webview/views/sections.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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', `<pre>${escapeHtml(hint.trim())}</pre>`) : '';
// hints the user opened, kept open when the diagnostics are rendered again
const openHints = new Set<string>();

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*/`
<details class="section hint-section"${key !== undefined ? ` data-hint-key="${escapeHtml(key)}"` : ''}${open ? ' open' : ''}>
<summary class="hint-summary">Hint</summary>
<pre>${escapeHtml(hint.trim())}</pre>
</details>
`;
}

export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/`
<button class="context-toggle-btn" data-context-toggle="${targetId}" aria-expanded="${isExpanded ? 'true' : 'false'}" type="button">
Expand All @@ -31,8 +52,13 @@ export const renderToggleSection = (title: string, targetId: string, isExpanded:
</button>
`;

export const renderDiagnosticHeader = (title: string, message: string): string => /*html*/
`<h3>${title}</h3><div class="diagnostic-header"><p>${message}</p></div>`;
export const renderDiagnosticHeader = (title: string, message: string, actions = ''): string => /*html*/`
<div class="diagnostic-title-row">
<h3>${title}</h3>
${actions.trim() ? `<div class="diagnostic-actions">${actions}</div>` : ''}
</div>
<div class="diagnostic-header"><p>${message}</p></div>
`;

export function renderDiagnosticDataAttributes(diagnostic: LJDiagnostic): string {
const target = getDiagnosticRevealTarget(diagnostic);
Expand Down
Loading