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 b8e6478..2780fa5 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -371,6 +371,8 @@ export function getStyles(): string { align-items: flex-start; gap: 0.5rem; min-width: 0; + padding: 0.0625rem 0.25rem; + border-radius: 3px; } .vc-line-content { flex: 0 1 auto; @@ -389,6 +391,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); } @@ -420,8 +468,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/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts new file mode 100644 index 0000000..928f14c --- /dev/null +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -0,0 +1,196 @@ +import type { VCImplication } from "../../../types/vc-implications"; +import { renderHighlightedInlineExpression } from "../../highlighting"; + +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; + +function getImplicationLines(node: VCImplication): string[] { + const lines: string[] = []; + for (let current: VCImplication | null = node; current; current = current.next) { + if ( + current.next + && (current.name === null || current.type === null || current.predicate === "true") + ) continue; + lines.push(current.predicate); + } + return lines; +} + +function renderVCLine(content: string, className = ""): string { + return /*html*/` +
+
${content}
+
+ `; +} + +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(renderChangedFragment(after)); + const change = renderDestinationTokenDiff(before, after); + return renderVCLine(change.content, change.hasAddedContent ? "" : "vc-change-line"); + }) + .join(""); +} + +export function renderImplication(node: VCImplication): string { + return getImplicationLines(node) + .map(predicate => renderVCLine(renderHighlightedInlineExpression(predicate))) + .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(renderHighlightedInlineExpression(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 2506c06..0942178 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -1,26 +1,12 @@ 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 - -function renderImplication(node: VCImplication): string { - const lines: string[] = []; - - 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; - - const content = /*binder - ? `∀${escapeHtml(current.name!)}: ${escapeHtml(current.type!)}. ${renderHighlightedInlineExpression(current.predicate)}` - :*/ renderHighlightedInlineExpression(current.predicate); - lines.push(`
${content}
`); - } - - return lines.join(""); -} +const stepIndexes = new Map(); // errorId => step index, preserved across re-renders +const simplificationSteps = new Map(); // errorId => simplification steps function renderStepButton(errorId: string, step: "previous" | "next", disabled: boolean): string { const label = `${step === "previous" ? "Previous" : "Next"} simplification`; @@ -34,16 +20,16 @@ function renderStepHeader( index: number, stepCount: number, ): string { - const chronologicalStep = stepCount - index; + const currStep = stepCount - index; const simplification = current.simplification?.trim(); - const label = simplification || "Original"; + const label = escapeHtml(simplification || "Original"); return /*html*/`
- ${escapeHtml(label)} + ${label}
- - ${chronologicalStep}/${stepCount} + + ${currStep}/${stepCount}
${renderStepButton(errorId, "previous", index === stepCount - 1)} @@ -54,16 +40,45 @@ function renderStepHeader( `; } +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 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; } @@ -83,15 +98,14 @@ export function renderVCImplication( for (let current: VCSimplificationResult | null = result; current; current = current.origin) { steps.push(current); } + simplificationSteps.set(errorId, steps); const index = Math.min(stepIndexes.get(errorId) ?? 0, steps.length - 1); stepIndexes.set(errorId, index); - const current = steps[index]; return /*html*/ `
- ${steps.length > 1 ? renderStepHeader(errorId, current, index, steps.length) : ""} -
${renderImplication(current.implication)}
+ ${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*/` `; }