From a486f4b1ab4aba297808426bf85d5deb3b56c5d1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 26 Jun 2026 10:49:10 +0100 Subject: [PATCH 01/10] Use Table Layout for VCs --- client/src/webview/styles.ts | 31 ++++++++----- .../webview/views/diagnostics/vc-changes.ts | 45 ++++++++++++++----- 2 files changed, 53 insertions(+), 23 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 2780fa5..93186c2 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -361,23 +361,32 @@ export function getStyles(): string { text-align: right; } .vc-chain { - display: flex; - flex-direction: column; - gap: 0.25rem; + display: table; + width: 100%; + border-spacing: 0 0.25rem; min-width: 0; } .vc-line { - display: flex; - align-items: flex-start; - gap: 0.5rem; - min-width: 0; - padding: 0.0625rem 0.25rem; - border-radius: 3px; + 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; diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 928f14c..c026a57 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -1,5 +1,6 @@ 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 }; @@ -7,23 +8,40 @@ 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 - && (current.name === null || current.type === null || current.predicate === "true") - ) continue; - lines.push(current.predicate); + if (current.next && !hasBinder(current)) continue; + lines.push(formatImplicationLine(current)); } return lines; } -function renderVCLine(content: string, className = ""): string { +function renderVCLine(line: string, className = "", predicateContent?: string): string { + const { binder, type, predicate } = parseImplicationLine(line); + const title = binder && type ? ` title="${escapeHtml(`${binder.slice(1)}: ${type}`)}"` : ""; + return /*html*/`
-
${content}
+
${escapeHtml(binder)}
+
${predicateContent ?? renderHighlightedInlineExpression(predicate)}
`; } @@ -158,16 +176,19 @@ function renderChangedDestinationLines(removed: string[], added: string[]): stri 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"); + 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(predicate => renderVCLine(renderHighlightedInlineExpression(predicate))) + .map(line => renderVCLine(line)) .join(""); } @@ -185,7 +206,7 @@ export function renderImplicationChange(before: VCImplication, after: VCImplicat for (const operation of operations) { if (operation.kind === "unchanged") { flushChanges(); - html += renderVCLine(renderHighlightedInlineExpression(operation.value)); + html += renderVCLine(operation.value); continue; } changed[operation.kind].push(operation.value); From 7fb5a46a2765a0c1c74e3659316540ba59c0e8e9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 26 Jun 2026 11:08:47 +0100 Subject: [PATCH 02/10] Show Binder Type on Hover --- client/src/webview/views/diagnostics/vc-changes.ts | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index c026a57..611d26c 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -36,11 +36,9 @@ function getImplicationLines(node: VCImplication): string[] { function renderVCLine(line: string, className = "", predicateContent?: string): string { const { binder, type, predicate } = parseImplicationLine(line); - const title = binder && type ? ` title="${escapeHtml(`${binder.slice(1)}: ${type}`)}"` : ""; - return /*html*/`
-
${escapeHtml(binder)}
+
${escapeHtml(binder)}
${predicateContent ?? renderHighlightedInlineExpression(predicate)}
`; From 1e0add806e6244e151bc489668b467526306c86f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 25 Jun 2026 10:36:08 +0100 Subject: [PATCH 03/10] Display Counterexample Assignments by Line --- .../views/diagnostics/counterexample.ts | 22 +++++++++++++++++++ .../src/webview/views/diagnostics/errors.ts | 3 ++- .../webview/views/diagnostics/vc-changes.ts | 2 +- 3 files changed, 25 insertions(+), 2 deletions(-) create mode 100644 client/src/webview/views/diagnostics/counterexample.ts diff --git a/client/src/webview/views/diagnostics/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts new file mode 100644 index 0000000..4202612 --- /dev/null +++ b/client/src/webview/views/diagnostics/counterexample.ts @@ -0,0 +1,22 @@ +import { renderHighlightedInlineExpression } from "../../highlighting"; +import { renderVCLine } from "./vc-changes"; + +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 => renderVCLine(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 index 611d26c..34a0333 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -34,7 +34,7 @@ function getImplicationLines(node: VCImplication): string[] { return lines; } -function renderVCLine(line: string, className = "", predicateContent?: string): string { +export function renderVCLine(line: string, className = "", predicateContent?: string): string { const { binder, type, predicate } = parseImplicationLine(line); return /*html*/`
From 930446aef2ed023f796b72f65edb6da1a46decd6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 25 Jun 2026 10:46:54 +0100 Subject: [PATCH 04/10] Display Simplified in Last Simplification Step --- client/src/webview/views/diagnostics/vc-implications.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 0942178..c2b76e6 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -22,7 +22,7 @@ function renderStepHeader( ): string { const currStep = stepCount - index; const simplification = current.simplification?.trim(); - const label = escapeHtml(simplification || "Original"); + const label = escapeHtml(index === 0 ? "Simplified" : simplification || "Original"); return /*html*/`
From 05c098b60b241f37e3de6d3062dd44e58df906b8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 26 Jun 2026 11:40:30 +0100 Subject: [PATCH 05/10] Fix Counterexample Rendering --- client/src/webview/styles.ts | 8 ++++++++ client/src/webview/views/diagnostics/counterexample.ts | 7 +++++-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 93186c2..f8dfbd9 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -366,6 +366,14 @@ export function getStyles(): string { border-spacing: 0 0.25rem; min-width: 0; } + .counterexample-container .vc-chain { + display: flex; + flex-direction: column; + gap: 0.25rem; + } + .counterexample-line { + overflow-wrap: anywhere; + } .vc-line { display: table-row; } diff --git a/client/src/webview/views/diagnostics/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts index 4202612..6d80f76 100644 --- a/client/src/webview/views/diagnostics/counterexample.ts +++ b/client/src/webview/views/diagnostics/counterexample.ts @@ -1,5 +1,4 @@ import { renderHighlightedInlineExpression } from "../../highlighting"; -import { renderVCLine } from "./vc-changes"; function getCounterexampleLines(counterexample: string): string[] { return counterexample @@ -15,7 +14,11 @@ export function renderCounterexample(counterexample: string): string { return /*html*/`
- ${lines.map(line => renderVCLine(renderHighlightedInlineExpression(line))).join("")} + ${lines.map(line => /*html*/` +
+ ${renderHighlightedInlineExpression(line)} +
+ `).join("")}
`; From 972738a53bb4aff02ca78042f736a78efb21ebe7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 27 Jun 2026 16:38:58 +0100 Subject: [PATCH 06/10] Fix Diagnostic Reveal --- client/src/services/webview.ts | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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; + } } }) ); From e7df79d7005a133c64dd62ce277fdb28bb8498e2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 14 Jul 2026 18:28:34 +0100 Subject: [PATCH 07/10] Minor Change --- client/src/webview/styles.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index f8dfbd9..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; From 2770bc15fe5dd056ccee405ddc29edf91b45e976 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 16 Jul 2026 12:15:38 +0100 Subject: [PATCH 08/10] Minor Fix --- client/src/webview/views/diagnostics/vc-changes.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts index 34a0333..67fa0ab 100644 --- a/client/src/webview/views/diagnostics/vc-changes.ts +++ b/client/src/webview/views/diagnostics/vc-changes.ts @@ -38,7 +38,7 @@ export function renderVCLine(line: string, className = "", predicateContent?: st const { binder, type, predicate } = parseImplicationLine(line); return /*html*/`
-
${escapeHtml(binder)}
+ ${binder ? /*html*/`
${escapeHtml(binder)}
` : ""}
${predicateContent ?? renderHighlightedInlineExpression(predicate)}
`; From da1780051e7dc08f5d1f1bd311892cfdb23a9c2c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 20 Jul 2026 16:14:18 +0100 Subject: [PATCH 09/10] Minor Fix --- client/src/webview/styles.ts | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index ff382cb..b1aefa9 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -361,9 +361,10 @@ export function getStyles(): string { text-align: right; } .vc-chain { - display: table; + display: grid; + grid-template-columns: max-content minmax(0, 1fr); + row-gap: 0.25rem; width: 100%; - border-spacing: 0 0.25rem; min-width: 0; } .counterexample-container .vc-chain { @@ -375,26 +376,25 @@ export function getStyles(): string { overflow-wrap: anywhere; } .vc-line { - display: table-row; + display: contents; } .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-predicate-cell:only-child { + grid-column: 1 / -1; } .vc-node { display: inline; From 8b353f68db737abe5897df0dcd56dc8eb507e52d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 20 Jul 2026 16:26:23 +0100 Subject: [PATCH 10/10] Minor Fix --- client/src/webview/styles.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index b1aefa9..769ab1f 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -362,7 +362,7 @@ export function getStyles(): string { } .vc-chain { display: grid; - grid-template-columns: max-content minmax(0, 1fr); + grid-template-columns: fit-content(40%) minmax(0, 1fr); row-gap: 0.25rem; width: 100%; min-width: 0; @@ -388,7 +388,7 @@ export function getStyles(): string { min-height: 1.2em; padding-right: 0.75rem; color: var(--vscode-descriptionForeground); - white-space: nowrap; + white-space: normal; } .vc-predicate-cell { color: var(--vscode-editor-foreground);