diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 9cc7f1f..2c03de4 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/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..c7c1219 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, @@ -402,10 +402,63 @@ 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('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')), 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('.hint-message')?.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.spec.ts b/client/src/webview/state-errors.spec.ts index 0c7c41f..b93de4a 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/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..be36de7 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -195,12 +195,58 @@ 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; + } + .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 { @@ -252,8 +298,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/diagnostics.spec.ts b/client/src/webview/views/diagnostics/diagnostics.spec.ts index 5b58a51..8d9d430 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 1b9db34..d79c611 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 { @@ -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 = renderHints(error.hints, 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..e718bc5 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 { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderHints, 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 = 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 3dd7b6d..bc1d02f 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"; @@ -21,8 +21,46 @@ 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 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 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*/` +
    + ${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*/` `; -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); diff --git a/server/src/main/java/dtos/diagnostics/HintDTO.java b/server/src/main/java/dtos/diagnostics/HintDTO.java new file mode 100644 index 0000000..8e1c6ed --- /dev/null +++ b/server/src/main/java/dtos/diagnostics/HintDTO.java @@ -0,0 +1,24 @@ +package dtos.diagnostics; + +import java.util.List; +import java.util.Locale; + +import liquidjava.diagnostics.hints.Hint; + +/** + * DTO for serializing a hint of a diagnostic, so clients can show each hint separately + * + * @param kind what the hint is about, e.g. {@code call-sequence} for calls that bring the object to a state that allows + * the failing call + * @param message the hint as shown to the user + */ +public record HintDTO(String kind, String message) { + + public static HintDTO from(Hint hint) { + return new HintDTO(hint.kind().name().toLowerCase(Locale.ROOT).replace('_', '-'), hint.message()); + } + + public static List from(List hints) { + return hints.stream().map(HintDTO::from).toList(); + } +} diff --git a/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java b/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java index 6b4ba86..d47e124 100644 --- a/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java +++ b/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java @@ -1,5 +1,7 @@ package dtos.diagnostics; +import java.util.List; + import liquidjava.diagnostics.LJDiagnostic; /** @@ -11,22 +13,22 @@ public class LJDiagnosticDTO { public final String type; public final String title; public final String message; - public final String hint; + public final List hints; public final String file; public final SourcePositionDTO position; public LJDiagnosticDTO(String category, String type, LJDiagnostic diagnostic) { - this(category, type, diagnostic.getTitle(), diagnostic.getMessage(), diagnostic.getHint(), + this(category, type, diagnostic.getTitle(), diagnostic.getMessage(), HintDTO.from(diagnostic.getHints()), diagnostic.getFile(), SourcePositionDTO.from(diagnostic.getPosition())); } - public LJDiagnosticDTO(String category, String type, String title, String message, String hint, String file, + public LJDiagnosticDTO(String category, String type, String title, String message, List hints, String file, SourcePositionDTO position) { this.category = category; this.type = type; this.title = title; this.message = message; - this.hint = hint; + this.hints = hints; this.file = file; this.position = position; } diff --git a/server/src/main/java/dtos/errors/LJErrorDTO.java b/server/src/main/java/dtos/errors/LJErrorDTO.java index 72803a0..9293491 100644 --- a/server/src/main/java/dtos/errors/LJErrorDTO.java +++ b/server/src/main/java/dtos/errors/LJErrorDTO.java @@ -1,5 +1,8 @@ package dtos.errors; +import java.util.List; + +import dtos.diagnostics.HintDTO; import dtos.diagnostics.LJDiagnosticDTO; import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.TranslationTableDTO; @@ -22,9 +25,9 @@ protected LJErrorDTO(String category, String type, LJError error) { this.translationTable = TranslationTableDTO.from(error.getTranslationTable()); } - public LJErrorDTO(String category, String type, String title, String message, String hint, String file, + public LJErrorDTO(String category, String type, String title, String message, List hints, String file, SourcePositionDTO position, TranslationTableDTO translationTable) { - super(category, type, title, message, hint, file, position); + super(category, type, title, message, hints, file, position); this.translationTable = translationTable; } diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java index 6de0095..f7c0d2e 100644 --- a/server/src/test/java/utils/DiagnosticConverterTest.java +++ b/server/src/test/java/utils/DiagnosticConverterTest.java @@ -10,6 +10,7 @@ import org.junit.jupiter.api.Test; import org.junit.jupiter.api.io.TempDir; +import dtos.diagnostics.HintDTO; import dtos.diagnostics.LJDiagnosticDTO; import dtos.diagnostics.SourcePositionDTO; import dtos.errors.*; @@ -55,11 +56,24 @@ void preservesCommonDiagnosticFields() throws Exception { assertEquals("custom-error", dto.type); assertEquals("Error", dto.title); assertEquals("verification failed", dto.message); - assertEquals("check the refinement", dto.hint); + assertEquals(List.of(new HintDTO("general", "check the refinement")), dto.hints); assertEquals(workspace.resolve("Example.java").toRealPath().toString(), dto.file); assertEquals(new SourcePositionDTO(dto.file, 1, 8, 1, 18), dto.position); } + @Test + void keepsEachHintWithItsKind() { + CustomError error = new CustomError("verification failed", position); + error.addHint(new Hint(Hint.Kind.CALL_SEQUENCE, "Call f.open() before this call to move f from created to open")); + error.addHint(new Hint(Hint.Kind.CALL_SEQUENCE, "Call f.reopen() before this call to move f from created to open")); + error.addHint(new Hint(Hint.Kind.AVAILABLE_CALLS, "In state created, f can call: open(), reopen()")); + LJDiagnosticDTO dto = (LJDiagnosticDTO) DiagnosticConverter.convertToDTO(error); + assertEquals(List.of( + new HintDTO("call-sequence", "Call f.open() before this call to move f from created to open"), + new HintDTO("call-sequence", "Call f.reopen() before this call to move f from created to open"), + new HintDTO("available-calls", "In state created, f can call: open(), reopen()")), dto.hints); + } + @Test void convertsIllegalConstructorTransitionToAnError() { LJDiagnosticDTO dto = (LJDiagnosticDTO) DiagnosticConverter.convertToDTO( @@ -122,7 +136,7 @@ void preservesWarningSpecificDetailsAndOverloadHint() { assertEquals("run()", missingMethod.signature); assertEquals("example.External", missingMethod.className); assertArrayEquals(new String[] { "run(int)", "run(String)" }, missingMethod.overloads); - assertEquals("Available overloads:\n run(int)\n run(String)", missingMethod.hint); + assertEquals(List.of(new HintDTO("general", "Available overloads:\n run(int)\n run(String)")), missingMethod.hints); UnsatisfiableRefinementWarningDTO unsatisfiable = (UnsatisfiableRefinementWarningDTO) DiagnosticConverter.convertToDTO( new UnsatisfiableRefinementWarning(position, "_ > 0 && _ < 0"));