diff --git a/client/src/services/webview.ts b/client/src/services/webview.ts index 0300adf..787f656 100644 --- a/client/src/services/webview.ts +++ b/client/src/services/webview.ts @@ -9,6 +9,7 @@ import type { DiagnosticRevealTarget } from "../types/diagnostics"; */ export function registerWebview(context: vscode.ExtensionContext) { extension.webview = new LiquidJavaWebviewProvider(context.extensionUri); + let pendingDiagnosticReveal: DiagnosticRevealTarget | undefined; // webview provider context.subscriptions.push( @@ -17,8 +18,15 @@ export function registerWebview(context: vscode.ExtensionContext) { // show view command context.subscriptions.push( vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget) => { + const isVisible = extension.webview?.isVisible(); await vscode.commands.executeCommand("liquidJavaView.focus"); - if (diagnostic) extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic }); + if (!diagnostic) return; + + if (isVisible) { + extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic }); + } else { + pendingDiagnosticReveal = diagnostic; + } }) ); // listen for messages from the webview @@ -30,6 +38,10 @@ export function registerWebview(context: vscode.ExtensionContext) { if (extension.context) extension.webview?.sendMessage({ type: "context", context: extension.context , errorAtCursor: extension.errorAtCursor }); if (extension.stateMachine) extension.webview?.sendMessage({ type: "fsm", sm: extension.stateMachine }); if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status }); + if (pendingDiagnosticReveal) { + extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic: pendingDiagnosticReveal }); + pendingDiagnosticReveal = undefined; + } } }) ); diff --git a/client/src/types/vc-implications.ts b/client/src/types/vc-implications.ts index 2ecc53a..a6750ed 100644 --- a/client/src/types/vc-implications.ts +++ b/client/src/types/vc-implications.ts @@ -8,4 +8,5 @@ export type VCImplication = { export type VCSimplificationResult = { implication: VCImplication; origin: VCSimplificationResult | null; + simplification: string | null; } diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index ca33de4..afc428c 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -135,9 +135,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const vcImplicationStepButton = target.closest?.('.vc-step-btn'); if (vcImplicationStepButton) { e.stopPropagation(); - if (handleVCImplicationStepClick(vcImplicationStepButton)) { - updateView(); - } + handleVCImplicationStepClick(vcImplicationStepButton); return; } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index fe9ee25..ff382cb 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -161,7 +161,7 @@ export function getStyles(): string { } .diagnostic-item { background-color: var(--vscode-textCodeBlock-background); - padding: 0.5rem 5rem 0.5rem 1rem; + padding: 0.5rem 1rem; margin-bottom: 1rem; border-radius: 4px; position: relative; @@ -324,28 +324,77 @@ export function getStyles(): string { } .vc-container { display: flex; - justify-content: space-between; - align-items: flex-start; - gap: 1rem; + flex-direction: column; + gap: 0.375rem; margin: 0.5rem 0; } + .vc-step-header { + display: flex; + align-items: center; + justify-content: space-between; + gap: 0.75rem; + min-width: 0; + padding-bottom: 0.25rem; + border-bottom: 1px solid var(--vscode-widget-border, var(--vscode-panel-border)); + font-family: var(--vscode-font-family); + font-size: 0.8rem; + line-height: 1.25rem; + } + .vc-step-name { + min-width: 0; + overflow: hidden; + color: var(--vscode-descriptionForeground); + font-weight: 600; + text-overflow: ellipsis; + white-space: nowrap; + } + .vc-step-navigation { + display: inline-flex; + align-items: center; + gap: 0.25rem; + flex-shrink: 0; + } + .vc-step-position { + min-width: 2.5rem; + color: var(--vscode-descriptionForeground); + font-variant-numeric: tabular-nums; + text-align: right; + } .vc-chain { - flex: 1; + display: table; + width: 100%; + border-spacing: 0 0.25rem; + min-width: 0; + } + .counterexample-container .vc-chain { display: flex; flex-direction: column; gap: 0.25rem; - min-width: 0; + } + .counterexample-line { + overflow-wrap: anywhere; } .vc-line { - display: flex; - align-items: flex-start; - gap: 0.5rem; - min-width: 0; + display: table-row; } - .vc-line-content { - flex: 0 1 auto; + .vc-binder-cell, + .vc-predicate-cell { + display: table-cell; min-width: 0; + padding: 0.0625rem 0.25rem; overflow-wrap: anywhere; + vertical-align: top; + } + .vc-binder-cell { + min-height: 1.2em; + padding-right: 0.75rem; + color: var(--vscode-descriptionForeground); + white-space: nowrap; + width: 1%; + } + .vc-predicate-cell { + color: var(--vscode-editor-foreground); + width: 99%; } .vc-node { display: inline; @@ -359,6 +408,52 @@ export function getStyles(): string { .vc-node:hover { background: none; } + .vc-change-line .vc-node { + border-radius: 2px; + animation: vc-change-line-fade 1.4s ease-out; + } + .vc-change-fragment { + border-radius: 2px; + animation: vc-change-fragment-fade 1.4s ease-out; + } + @keyframes vc-change-line-fade { + 0% { + background-color: rgba(255, 255, 96, 0.68); + box-shadow: 0 0 0 1px rgba(255, 255, 0, 0.38); + } + 18% { + background-color: rgba(255, 255, 0, 0.4); + box-shadow: 0 0 0 1px rgba(255, 255, 0, 0.2); + } + 100% { + background-color: transparent; + box-shadow: none; + } + } + @keyframes vc-change-fragment-fade { + 0% { + background-color: rgba(255, 255, 96, 0.68); + box-shadow: 0 0 0 1px rgba(255, 255, 0, 0.38); + } + 18% { + background-color: rgba(255, 255, 0, 0.4); + box-shadow: 0 0 0 1px rgba(255, 255, 0, 0.2); + } + 100% { + background-color: transparent; + box-shadow: none; + } + } + @media (prefers-reduced-motion: reduce) { + .vc-change-line .vc-node { + background-color: rgba(255, 255, 0, 0.3); + animation: none; + } + .vc-change-fragment { + background-color: rgba(255, 255, 0, 0.3); + animation: none; + } + } .vc-binder { color: var(--vscode-descriptionForeground); } @@ -390,8 +485,8 @@ export function getStyles(): string { } .vc-step-btn:hover { font-weight: bold; - background-color: transparent; opacity: 1; + background-color: transparent; } .vc-step-btn:disabled { cursor: default; diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index ae1d763..89324e5 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -2,7 +2,7 @@ import { LJVariable } from "../../../types/context"; import { RefinementMismatchError } from "../../../types/diagnostics"; import { renderHighlightedInlineExpression } from "../../highlighting"; import { escapeHtml, getSimpleName } from "../../utils"; -import { renderToggleSection, renderHighlightButton, renderDiagnosticRevealButton } from "../sections"; +import { renderToggleSection, renderVariableHighlightButton, renderDiagnosticRevealButton } from "../sections"; export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string { const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {})); @@ -24,11 +24,10 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool ${variables.map(variable => { - const displayName = getSimpleName(variable.name); const isRelevant = relevantNames.has(variable.name); return /*html*/` - ${renderHighlightButton(variable.position!, displayName)} + ${renderVariableHighlightButton(variable)} ${renderHighlightedInlineExpression(variable.refinement)} `}).join('')} diff --git a/client/src/webview/views/diagnostics/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts new file mode 100644 index 0000000..6d80f76 --- /dev/null +++ b/client/src/webview/views/diagnostics/counterexample.ts @@ -0,0 +1,25 @@ +import { renderHighlightedInlineExpression } from "../../highlighting"; + +function getCounterexampleLines(counterexample: string): string[] { + return counterexample + .split("&&") + .map(assignment => assignment.trim()) + .filter(Boolean); +} + +export function renderCounterexample(counterexample: string): string { + const lines = getCounterexampleLines(counterexample); + if (lines.length === 0) return ""; + + return /*html*/` +
+
+ ${lines.map(line => /*html*/` +
+ ${renderHighlightedInlineExpression(line)} +
+ `).join("")} +
+
+ `; +} diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index c777a32..ac48c74 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -1,4 +1,5 @@ import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton } from "../sections"; +import { renderCounterexample } from "./counterexample"; import { renderVCImplication } from "./vc-implications"; import type { ArgumentMismatchError, @@ -36,7 +37,7 @@ const errorContentRenderers: ErrorRendererMap = { 'refinement-error': (e: RefinementError) => /*html*/ ` ${renderExpressionSection('Expected', e.expected)} ${renderCustomSection('Found', renderVCImplication(e, e.found))} - ${e.counterexample ? renderExpressionSection('Counterexample', e.counterexample) : ''} + ${e.counterexample ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample)) : ''} `, 'state-refinement-error': (e: StateRefinementError) => /*html*/ ` ${renderExpressionSection('Expected', e.expected)} diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts new file mode 100644 index 0000000..67fa0ab --- /dev/null +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -0,0 +1,215 @@ +import type { VCImplication } from "../../../types/vc-implications"; +import { renderHighlightedInlineExpression } from "../../highlighting"; +import { escapeHtml } from "../../utils"; + +type ChangeKind = "unchanged" | "removed" | "added"; +type DiffOperation = { kind: ChangeKind; value: T }; + +const MIN_LINE_SIMILARITY = 0.3; +const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu; +const WHITESPACE_PATTERN = /^\s+$/u; +const VC_LINE_SEPARATOR = "\t"; + +function hasBinder(node: VCImplication): boolean { + return typeof node.name === "string" && node.name.length > 0; +} + +function formatImplicationLine(node: VCImplication): string { + const binder = hasBinder(node) ? `∀${node.name}` : ""; + const type = typeof node.type === "string" ? node.type : ""; + return [binder, type, node.predicate].join(VC_LINE_SEPARATOR); +} + +function parseImplicationLine(line: string): { binder: string; type: string; predicate: string } { + const [binder = "", type = "", predicate = ""] = line.split(VC_LINE_SEPARATOR); + return { binder, type, predicate }; +} + +function getImplicationLines(node: VCImplication): string[] { + const lines: string[] = []; + for (let current: VCImplication | null = node; current; current = current.next) { + if (current.next && !hasBinder(current)) continue; + lines.push(formatImplicationLine(current)); + } + return lines; +} + +export function renderVCLine(line: string, className = "", predicateContent?: string): string { + const { binder, type, predicate } = parseImplicationLine(line); + return /*html*/` +
+ ${binder ? /*html*/`
${escapeHtml(binder)}
` : ""} +
${predicateContent ?? renderHighlightedInlineExpression(predicate)}
+
+ `; +} + +function createMatrix(rows: number, columns: number): number[][] { + return Array.from({ length: rows + 1 }, () => new Array(columns + 1).fill(0)); +} + +function diffSequence(before: T[], after: T[]): DiffOperation[] { + const lengths = createMatrix(before.length, after.length); + + for (let beforeIndex = before.length - 1; beforeIndex >= 0; beforeIndex -= 1) { + for (let afterIndex = after.length - 1; afterIndex >= 0; afterIndex -= 1) { + lengths[beforeIndex][afterIndex] = before[beforeIndex] === after[afterIndex] + ? lengths[beforeIndex + 1][afterIndex + 1] + 1 + : Math.max(lengths[beforeIndex + 1][afterIndex], lengths[beforeIndex][afterIndex + 1]); + } + } + + const operations: DiffOperation[] = []; + let beforeIndex = 0; + let afterIndex = 0; + while (beforeIndex < before.length && afterIndex < after.length) { + if (before[beforeIndex] === after[afterIndex]) { + operations.push({ kind: "unchanged", value: before[beforeIndex] }); + beforeIndex++; + afterIndex++; + } else if (lengths[beforeIndex + 1][afterIndex] >= lengths[beforeIndex][afterIndex + 1]) { + operations.push({ kind: "removed", value: before[beforeIndex++] }); + } else { + operations.push({ kind: "added", value: after[afterIndex++] }); + } + } + operations.push( + ...before.slice(beforeIndex).map(value => ({ kind: "removed" as const, value })), + ...after.slice(afterIndex).map(value => ({ kind: "added" as const, value })), + ); + return operations; +} + +function tokenizeExpression(expression: string): string[] { + return expression.match(TOKEN_PATTERN) || []; +} + +function renderChangedFragment(content: string): string { + return `${renderHighlightedInlineExpression(content)}`; +} + +function renderDestinationTokenDiff(before: string, after: string): { content: string; hasAddedContent: boolean } { + const operations = diffSequence(tokenizeExpression(before), tokenizeExpression(after)); + let html = ""; + let changedContent = ""; + let hasAddedContent = false; + + const flushChangedContent = () => { + if (!changedContent) return; + const trailingWhitespace = changedContent.match(/\s+$/u)?.[0] ?? ""; + const content = changedContent.slice(0, changedContent.length - trailingWhitespace.length); + if (content) html += renderChangedFragment(content); + html += trailingWhitespace; + changedContent = ""; + }; + + operations.forEach((operation, index) => { + if (operation.kind === "added") { + changedContent += operation.value; + hasAddedContent = true; + return; + } + if (operation.kind === "unchanged") { + if (WHITESPACE_PATTERN.test(operation.value) && changedContent && operations[index + 1]?.kind === "added") { + changedContent += operation.value; + return; + } + flushChangedContent(); + html += renderHighlightedInlineExpression(operation.value); + } + }); + flushChangedContent(); + return { content: html, hasAddedContent }; +} + +function getLineSimilarity(before: string, after: string): number { + const beforeTokens = tokenizeExpression(before).filter(token => !WHITESPACE_PATTERN.test(token)); + const afterTokens = tokenizeExpression(after).filter(token => !WHITESPACE_PATTERN.test(token)); + const unchangedLength = diffSequence(beforeTokens, afterTokens) + .filter(operation => operation.kind === "unchanged") + .reduce((length, operation) => length + operation.value.length, 0); + const totalLength = Math.max(beforeTokens.join("").length, afterTokens.join("").length); + return totalLength === 0 ? 0 : unchangedLength / totalLength; +} + +function alignChangedLines(removed: string[], added: string[]): Array<[string | undefined, string | undefined]> { + const similarities = removed.map(before => added.map(after => getLineSimilarity(before, after))); + const scores = createMatrix(removed.length, added.length); + + for (let i = removed.length - 1; i >= 0; i -= 1) { + for (let j = added.length - 1; j >= 0; j -= 1) { + const similarity = similarities[i][j]; + scores[i][j] = Math.max( + scores[i + 1][j], + scores[i][j + 1], + similarity >= MIN_LINE_SIMILARITY ? similarity + scores[i + 1][j + 1] : 0, + ); + } + } + + const lines: Array<[string | undefined, string | undefined]> = []; + let i = 0; + let j = 0; + while (i < removed.length && j < added.length) { + const similarity = similarities[i][j]; + if ( + similarity >= MIN_LINE_SIMILARITY + && scores[i][j] === similarity + scores[i + 1][j + 1] + ) { + lines.push([removed[i++], added[j++]]); + } else if (scores[i][j + 1] >= scores[i + 1][j]) { + lines.push([undefined, added[j++]]); + } else { + lines.push([removed[i++], undefined]); + } + } + while (i < removed.length) lines.push([removed[i++], undefined]); + while (j < added.length) lines.push([undefined, added[j++]]); + return lines; +} + +function renderChangedDestinationLines(removed: string[], added: string[]): string { + if (added.length === 0) return ""; + + return alignChangedLines(removed, added) + .map(([before, after]) => { + if (after === undefined) return ""; + if (before === undefined) return renderVCLine(after, "vc-change-line"); + const change = renderDestinationTokenDiff( + parseImplicationLine(before).predicate, + parseImplicationLine(after).predicate, + ); + return renderVCLine(after, change.hasAddedContent ? "" : "vc-change-line", change.content); + }) + .join(""); +} + +export function renderImplication(node: VCImplication): string { + return getImplicationLines(node) + .map(line => renderVCLine(line)) + .join(""); +} + +export function renderImplicationChange(before: VCImplication, after: VCImplication): string { + const operations = diffSequence(getImplicationLines(before), getImplicationLines(after)); + let html = ""; + const changed = { removed: [] as string[], added: [] as string[] }; + + const flushChanges = () => { + html += renderChangedDestinationLines(changed.removed, changed.added); + changed.removed.length = 0; + changed.added.length = 0; + }; + + for (const operation of operations) { + if (operation.kind === "unchanged") { + flushChanges(); + html += renderVCLine(operation.value); + continue; + } + changed[operation.kind].push(operation.value); + } + + flushChanges(); + return html; +} diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 848220b..c2b76e6 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -1,43 +1,84 @@ import type { RefinementMismatchError } from "../../../types/diagnostics"; -import type { VCImplication, VCSimplificationResult } from "../../../types/vc-implications"; -import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../../highlighting"; +import type { VCSimplificationResult } from "../../../types/vc-implications"; +import { renderHighlightedExpression } from "../../highlighting"; import { renderCodicon } from "../../icons"; import { escapeHtml } from "../../utils"; +import { renderImplication, renderImplicationChange } from "./vc-changes"; -const stepIndexes = new Map(); // step index => errorId to preserve step state across re-renders +const stepIndexes = new Map(); // errorId => step index, preserved across re-renders +const simplificationSteps = new Map(); // errorId => simplification steps -function renderImplication(node: VCImplication): string { - const lines: string[] = []; +function renderStepButton(errorId: string, step: "previous" | "next", disabled: boolean): string { + const label = `${step === "previous" ? "Previous" : "Next"} simplification`; + const icon = step === "previous" ? "arrow-small-left" : "arrow-small-right"; + return ``; +} - for (let current: VCImplication | null = node; current; current = current.next) { - const binder = current.name !== null && current.type !== null; - if (!binder && current.next || current.predicate === "true" && current.next !== null) continue; +function renderStepHeader( + errorId: string, + current: VCSimplificationResult, + index: number, + stepCount: number, +): string { + const currStep = stepCount - index; + const simplification = current.simplification?.trim(); + const label = escapeHtml(index === 0 ? "Simplified" : simplification || "Original"); - const content = /*binder - ? `∀${escapeHtml(current.name!)}: ${escapeHtml(current.type!)}. ${renderHighlightedInlineExpression(current.predicate)}` - :*/ renderHighlightedInlineExpression(current.predicate); - lines.push(`
${content}
`); - } + return /*html*/` +
+ ${label} +
+ + ${currStep}/${stepCount} + +
+ ${renderStepButton(errorId, "previous", index === stepCount - 1)} + ${renderStepButton(errorId, "next", index === 0)} +
+
+
+ `; +} - return lines.join(""); +function getTargetStepIndex(errorId: string, step: string | null): number | undefined { + const steps = simplificationSteps.get(errorId); + if (!steps) return; + + const index = stepIndexes.get(errorId) ?? 0; + const targetIndex = step === "previous" ? index + 1 : step === "next" ? index - 1 : -1; + if (targetIndex < 0 || targetIndex >= steps.length) return; + return targetIndex; } -function renderStepButton(errorId: string, step: "previous" | "next", disabled: boolean): string { - const label = `${step === "previous" ? "Previous" : "Next"} simplification`; - const icon = step === "previous" ? "arrow-small-left" : "arrow-small-right"; - return ``; +function renderSelectedStep(errorId: string, previousIndex?: number): string { + const steps = simplificationSteps.get(errorId); + if (!steps) return ""; + + const index = Math.min(stepIndexes.get(errorId) ?? 0, steps.length - 1); + const current = steps[index]; + const previous = previousIndex === undefined ? undefined : steps[previousIndex]; + const implication = previous + ? `
${renderImplicationChange(previous.implication, current.implication)}
` + : `
${renderImplication(current.implication)}
`; + + return /*html*/` + ${steps.length > 1 ? renderStepHeader(errorId, current, index, steps.length) : ""} + ${implication} + `; } export function handleVCImplicationStepClick(target: Element): boolean { const errorId = target.getAttribute("data-error-id"); const step = target.getAttribute("data-vc-step"); - if (!errorId || target.hasAttribute("disabled")) return false; + if (!errorId || (target as HTMLButtonElement).disabled) return false; - const index = stepIndexes.get(errorId) ?? 0; - const nextIndex = step === "previous" ? index + 1 : step === "next" ? index - 1 : -1; - if (nextIndex < 0) return false; + const currentIndex = stepIndexes.get(errorId) ?? 0; + const targetIndex = getTargetStepIndex(errorId, step); + const container = target.closest?.(".vc-container"); + if (targetIndex === undefined) return false; - stepIndexes.set(errorId, nextIndex); + stepIndexes.set(errorId, targetIndex); + if (container) container.innerHTML = renderSelectedStep(errorId, currentIndex); return true; } @@ -53,21 +94,18 @@ export function renderVCImplication( error.title, error.message ])); - const history: VCSimplificationResult[] = []; + const steps: VCSimplificationResult[] = []; for (let current: VCSimplificationResult | null = result; current; current = current.origin) { - history.push(current); + steps.push(current); } + simplificationSteps.set(errorId, steps); - const index = Math.min(stepIndexes.get(errorId) ?? 0, history.length - 1); + const index = Math.min(stepIndexes.get(errorId) ?? 0, steps.length - 1); stepIndexes.set(errorId, index); return /*html*/ `
-
${renderImplication(history[index].implication)}
-
- ${renderStepButton(errorId, "previous", index === history.length - 1)} - ${renderStepButton(errorId, "next", index === 0)} -
+ ${renderSelectedStep(errorId)}
`; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index fba3f27..2b8c16e 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -1,8 +1,9 @@ import type { LJDiagnostic, SourcePosition } from "../../types/diagnostics"; -import { escapeHtml } from "../utils"; +import { escapeHtml, getSimpleName } from "../utils"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../highlighting"; import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal"; import { renderCodicon, renderCodiconButton } from "../icons"; +import { LJVariable } from "../../types/context"; export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
@@ -40,17 +41,21 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => { return renderCustomSection("Location", /*html*/`
${renderLocationLink(diagnostic.position)}
`); }; -export function renderHighlightButton(position: SourcePosition, content: string, error: boolean = false): string { +export function renderVariableHighlightButton(variable: LJVariable): string { + const displayName = getSimpleName(variable.name); + const position = variable.position; + if (!position || !position.file) return `${displayName}`; return /*html*/` `; } diff --git a/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java index 155c3ac..0dc9d26 100644 --- a/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java +++ b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java @@ -5,7 +5,7 @@ /** * DTO for serializing a simplified VC and its complete predecessor states. */ -public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin) { +public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin, String simplification) { public static VCSimplificationResultDTO from(VCSimplificationResult result) { if (result == null) @@ -13,6 +13,8 @@ public static VCSimplificationResultDTO from(VCSimplificationResult result) { return new VCSimplificationResultDTO( VCImplicationDTO.from(result.getImplication()), - from(result.getOrigin())); + from(result.getOrigin()), + result.getSimplification() + ); } }