From 41980f33ff43b65df2a1bcb3ea77ad7931eef635 Mon Sep 17 00:00:00 2001
From: Ricardo Costa <rcosta.ms358@gmail.com>
Date: Sun, 9 Aug 2026 14:50:23 +0100
Subject: [PATCH] Highlight VC Binders

---
 client/src/webview/script.ts                  |  5 +-
 client/src/webview/styles.ts                  |  7 +++
 .../webview/views/diagnostics/vc-changes.ts   | 53 +++++++++++++----
 .../views/diagnostics/vc-implications.ts      | 58 +++++++++++--------
 client/src/webview/views/sections.ts          | 21 +++++--
 5 files changed, 104 insertions(+), 40 deletions(-)

diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts
index afc428c..d3e5cd1 100644
--- a/client/src/webview/script.ts
+++ b/client/src/webview/script.ts
@@ -135,7 +135,10 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
         const vcImplicationStepButton = target.closest?.('.vc-step-btn');
         if (vcImplicationStepButton) {
             e.stopPropagation();
-            handleVCImplicationStepClick(vcImplicationStepButton);
+            handleVCImplicationStepClick(vcImplicationStepButton, () => {
+                root.querySelector<HTMLElement>('.highlight-var-btn.selected')?.classList.remove('selected');
+                vscode.postMessage({ type: 'highlight', range: null });
+            });
             return;
         }
 
diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
index 769ab1f..12fc480 100644
--- a/client/src/webview/styles.ts
+++ b/client/src/webview/styles.ts
@@ -728,6 +728,13 @@ export function getStyles(): string {
         .highlight-var-btn.selected {
             background-color: var(--vscode-button-background);
         }
+        .vc-binder.highlight-var-btn {
+            margin: 0;
+            padding: 0 0.15rem;
+        }
+        .vc-binder.highlight-var-btn.selected {
+            color: var(--lj-token-identifier);
+        }
         .highlight-var-btn.error,
         .diagnostic-reveal-btn.error {
             background-color: color-mix(in srgb, var(--vscode-errorForeground) 80%, transparent);
diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts
index 67fa0ab..7ff74ba 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -1,6 +1,8 @@
 import type { VCImplication } from "../../../types/vc-implications";
+import type { TranslationTable } from "../../../types/diagnostics";
 import { renderHighlightedInlineExpression } from "../../highlighting";
 import { escapeHtml } from "../../utils";
+import { renderSourceHighlightButton } from "../sections";
 
 type ChangeKind = "unchanged" | "removed" | "added";
 type DiffOperation<T> = { kind: ChangeKind; value: T };
@@ -34,11 +36,29 @@ function getImplicationLines(node: VCImplication): string[] {
     return lines;
 }
 
-export function renderVCLine(line: string, className = "", predicateContent?: string): string {
+function renderBinder(binder: string, type: string, translationTable?: TranslationTable): string {
+    const placement = translationTable?.[binder.slice(1)];
+    if (!placement?.position?.file) {
+        return `<span class="vc-node vc-binder" title="${escapeHtml(type)}">${escapeHtml(binder)}</span>`;
+    }
+    return renderSourceHighlightButton(
+        escapeHtml(binder),
+        type,
+        placement.position,
+        "vc-node vc-binder",
+    );
+}
+
+export function renderVCLine(
+    line: string,
+    className = "",
+    predicateContent?: string,
+    translationTable?: TranslationTable,
+): string {
     const { binder, type, predicate } = parseImplicationLine(line);
     return /*html*/`
         <div class="vc-line ${className}">
-            ${binder ? /*html*/`<div class="vc-binder-cell"><span class="vc-node vc-binder" title="${type}">${escapeHtml(binder)}</span></div>` : ""}
+            ${binder ? /*html*/`<div class="vc-binder-cell">${renderBinder(binder, type, translationTable)}</div>` : ""}
             <div class="vc-predicate-cell"><span class="vc-node">${predicateContent ?? renderHighlightedInlineExpression(predicate)}</span></div>
         </div>
     `;
@@ -168,35 +188,48 @@ function alignChangedLines(removed: string[], added: string[]): Array<[string |
     return lines;
 }
 
-function renderChangedDestinationLines(removed: string[], added: string[]): string {
+function renderChangedDestinationLines(
+    removed: string[],
+    added: string[],
+    translationTable?: TranslationTable,
+): 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");
+            if (before === undefined) return renderVCLine(after, "vc-change-line", undefined, translationTable);
             const change = renderDestinationTokenDiff(
                 parseImplicationLine(before).predicate,
                 parseImplicationLine(after).predicate,
             );
-            return renderVCLine(after, change.hasAddedContent ? "" : "vc-change-line", change.content);
+            return renderVCLine(
+                after,
+                change.hasAddedContent ? "" : "vc-change-line",
+                change.content,
+                translationTable,
+            );
         })
         .join("");
 }
 
-export function renderImplication(node: VCImplication): string {
+export function renderImplication(node: VCImplication, translationTable?: TranslationTable): string {
     return getImplicationLines(node)
-        .map(line => renderVCLine(line))
+        .map(line => renderVCLine(line, "", undefined, translationTable))
         .join("");
 }
 
-export function renderImplicationChange(before: VCImplication, after: VCImplication): string {
+export function renderImplicationChange(
+    before: VCImplication,
+    after: VCImplication,
+    translationTable?: TranslationTable,
+): 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);
+        html += renderChangedDestinationLines(changed.removed, changed.added, translationTable);
         changed.removed.length = 0;
         changed.added.length = 0;
     };
@@ -204,7 +237,7 @@ export function renderImplicationChange(before: VCImplication, after: VCImplicat
     for (const operation of operations) {
         if (operation.kind === "unchanged") {
             flushChanges();
-            html += renderVCLine(operation.value);
+            html += renderVCLine(operation.value, "", undefined, translationTable);
             continue;
         }
         changed[operation.kind].push(operation.value);
diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts
index c2b76e6..f433e2b 100644
--- a/client/src/webview/views/diagnostics/vc-implications.ts
+++ b/client/src/webview/views/diagnostics/vc-implications.ts
@@ -1,12 +1,18 @@
-import type { RefinementMismatchError } from "../../../types/diagnostics";
+import type { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics";
 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<string, number>(); // errorId => step index, preserved across re-renders
-const simplificationSteps = new Map<string, VCSimplificationResult[]>(); // errorId => simplification steps
+// state to preserve across re-renders
+type VCState = {
+    steps: VCSimplificationResult[];
+    translationTable: TranslationTable;
+    stepIndex: number;
+};
+
+const vcStates = new Map<string, VCState>(); // errorId => VCState
 
 function renderStepButton(errorId: string, step: "previous" | "next", disabled: boolean): string {
     const label = `${step === "previous" ? "Previous" : "Next"} simplification`;
@@ -40,45 +46,49 @@ 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;
+function getTargetStepIndex(state: VCState, step: string | null): number | undefined {
+    const targetIndex = step === "previous"
+        ? state.stepIndex + 1
+        : step === "next"
+            ? state.stepIndex - 1
+            : -1;
+    if (targetIndex < 0 || targetIndex >= state.steps.length) return;
     return targetIndex;
 }
 
 function renderSelectedStep(errorId: string, previousIndex?: number): string {
-    const steps = simplificationSteps.get(errorId);
-    if (!steps) return "";
+    const state = vcStates.get(errorId);
+    if (!state) return "";
 
-    const index = Math.min(stepIndexes.get(errorId) ?? 0, steps.length - 1);
-    const current = steps[index];
+    const { steps, translationTable, stepIndex } = state;
+    const current = steps[stepIndex];
     const previous = previousIndex === undefined ? undefined : steps[previousIndex];
     const implication = previous
-        ? `<div class="vc-chain">${renderImplicationChange(previous.implication, current.implication)}</div>`
-        : `<div class="vc-chain">${renderImplication(current.implication)}</div>`;
+        ? `<div class="vc-chain">${renderImplicationChange(previous.implication, current.implication, translationTable)}</div>`
+        : `<div class="vc-chain">${renderImplication(current.implication, translationTable)}</div>`;
 
     return /*html*/`
-        ${steps.length > 1 ? renderStepHeader(errorId, current, index, steps.length) : ""}
+        ${steps.length > 1 ? renderStepHeader(errorId, current, stepIndex, steps.length) : ""}
         ${implication}
     `;
 }
 
-export function handleVCImplicationStepClick(target: Element): boolean {
+export function handleVCImplicationStepClick(target: Element, onStepChanged?: () => void): boolean {
     const errorId = target.getAttribute("data-error-id");
     const step = target.getAttribute("data-vc-step");
     if (!errorId || (target as HTMLButtonElement).disabled) return false;
 
-    const currentIndex = stepIndexes.get(errorId) ?? 0;
-    const targetIndex = getTargetStepIndex(errorId, step);
+    const state = vcStates.get(errorId);
+    if (!state) return false;
+
+    const currentIndex = state.stepIndex;
+    const targetIndex = getTargetStepIndex(state, step);
     const container = target.closest?.(".vc-container");
     if (targetIndex === undefined) return false;
 
-    stepIndexes.set(errorId, targetIndex);
+    state.stepIndex = targetIndex;
     if (container) container.innerHTML = renderSelectedStep(errorId, currentIndex);
+    onStepChanged?.();
     return true;
 }
 
@@ -98,10 +108,8 @@ 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 stepIndex = Math.min(vcStates.get(errorId)?.stepIndex ?? 0, steps.length - 1);
+    vcStates.set(errorId, { steps, translationTable: error.translationTable, stepIndex });
 
     return /*html*/ `
         <div class="container vc-container" data-error-id="${errorId}">
diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts
index 2b8c16e..4ca1ee3 100644
--- a/client/src/webview/views/sections.ts
+++ b/client/src/webview/views/sections.ts
@@ -45,17 +45,30 @@ export function renderVariableHighlightButton(variable: LJVariable): string {
     const displayName = getSimpleName(variable.name);
     const position = variable.position;
     if (!position || !position.file) return `<code>${displayName}</code>`;
+    return renderSourceHighlightButton(
+        `<code>${renderHighlightedInlineExpression(displayName)}</code>`,
+        variable.type,
+        position,
+    );
+}
+
+export function renderSourceHighlightButton(
+    content: string,
+    title: string,
+    position: SourcePosition & { file: string },
+    className = "",
+): string {
     return /*html*/`
         <button
-            class="highlight-var-btn"
-            title="${variable.type}"
+            class="highlight-var-btn${className ? ` ${className}` : ""}"
+            title="${escapeHtml(title)}"
             data-start-line="${position.lineStart}"
             data-start-column="${position.colStart}"
             data-end-line="${position.lineEnd}"
             data-end-column="${position.colEnd}"
-            data-file="${position.file}"
+            data-file="${escapeHtml(position.file)}"
         >
-            <code>${renderHighlightedInlineExpression(displayName)}</code>
+            ${content}
         </button>
     `;
 }