Wrap the Verification panel at spaces and operators, one conjunct per line

client/src/webview/highlighting.ts

@@ -98,6 +98,103 @@ export function renderHighlightedExpression(expression: string): string {
     return renderExpression(expression, true);
 }
 
+const WEAKER_THAN_AND = ["||", "-->", "?"];
+
+// the positions of the characters outside parentheses and string or character literals
+function topLevelIndices(expression: string): number[] {
+    const indices: number[] = [];
+    let depth = 0;
+    let quote: string | null = null;
+    for (let i = 0; i < expression.length; i++) {
+        if (quote) {
+            if (expression[i] === "\\") i++;
+            else if (expression[i] === quote) quote = null;
+        }
+        else if (expression[i] === '"' || expression[i] === "'") quote = expression[i];
+        else if (expression[i] === "(") depth++;
+        else if (expression[i] === ")") depth--;
+        else if (depth === 0) indices.push(i);
+    }
+    return indices;
+}
+
+/**
+ * Splits an expression at its top-level &&, keeping the && at the end of each conjunct but the last. An && inside
+ * parentheses or a literal stays in its conjunct, and nothing is split when a weaker operator (||, -->, ?:)
+ * outside them would make the parts look like conjuncts of the whole expression
+ */
+function splitConjuncts(expression: string): string[] {
+    const indices = topLevelIndices(expression);
+    if (indices.some(i => WEAKER_THAN_AND.some(operator => expression.startsWith(operator, i)))) return [expression.trim()];
+
+    const conjuncts: string[] = [];
+    let start = 0;
+    for (const i of indices) {
+        if (i < start || !expression.startsWith("&&", i)) continue;
+        conjuncts.push(expression.slice(start, i + 2).trim());
+        start = i + 2;
+    }
+    const last = expression.slice(start).trim();
+    return last ? [...conjuncts, last] : conjuncts;
+}
+
+// the condition and the two branches of an expression that is a conditional outside parentheses, or null
+function splitConditional(expression: string): [string, string, string] | null {
+    const indices = topLevelIndices(expression);
+    const question = indices.find(i => expression[i] === "?");
+    if (question === undefined) return null;
+
+    let nested = 0;
+    for (const i of indices.filter(i => i > question)) {
+        if (expression[i] === "?") nested++;
+        else if (expression[i] === ":" && nested-- === 0)
+            return [expression.slice(0, question), expression.slice(question + 1, i), expression.slice(i + 1)]
+                .map(part => part.trim()) as [string, string, string];
+    }
+    return null;
+}
+
+export type ExpressionLine = { text: string; branch: boolean };
+
+/**
+ * The lines an expression is shown on: one per top-level conjunct, and a conditional's condition with each branch
+ * on a line of its own, indented
+ */
+export function getExpressionLines(expression: string): ExpressionLine[] {
+    return splitConjuncts(expression).flatMap(conjunct => {
+        const conditional = splitConditional(conjunct);
+        if (!conditional) return [{ text: conjunct, branch: false }];
+        const [condition, then, otherwise] = conditional;
+        return [{ text: condition, branch: false }, { text: `? ${then}`, branch: true }, { text: `: ${otherwise}`, branch: true }];
+    });
+}
+
+/**
+ * Renders the lines of an expression, each of which wraps with a hanging indent
+ * @param renderText renders the text of the line at an index, highlighted by default
+ * @param trailing html shown at the end of the last line
+ */
+export function renderExpressionLines(
+    lines: ExpressionLine[],
+    renderText: (text: string, index: number) => string = renderHighlightedContent,
+    trailing = "",
+): string {
+    return lines.map((line, index) => {
+        const end = index === lines.length - 1 ? trailing : "";
+        return `<span class="lj-line${line.branch ? " lj-line-branch" : ""}">${renderText(line.text, index)}${end}</span>`;
+    }).join("");
+}
+
+/**
+ * Renders an expression on the lines of getExpressionLines, in an expression block as renderHighlightedExpression does
+ */
+export function renderHighlightedLines(expression: string): string {
+    if (!expression) return "";
+
+    const html = renderExpressionLines(getExpressionLines(expression));
+    return `<pre class="lj-expression-block"><code class="lj-expression-code">${html}</code></pre>`;
+}
+
 export function renderHighlightedInlineExpression(expression: string): string {
     return renderExpression(expression, false);
 }

client/src/webview/styles.spec.ts

@@ -105,6 +105,14 @@ describe('state error styles', () => {
         }
     });
 
+    it('breaks a Found line inside a name only when the name alone is wider than the line', () => {
+        render('');
+        document.body.insertAdjacentHTML('beforeend', '<div class="vc-binder-cell"></div><div class="vc-predicate-cell"></div>');
+
+        expect(style('.vc-binder-cell').overflowWrap).toBe('break-word');
+        expect(style('.vc-predicate-cell').overflowWrap).toBe('break-word');
+    });
+
     it('keeps other states with the default outline', () => {
         render(state(''));
 

client/src/webview/styles.ts

@@ -392,6 +392,14 @@ export function getStyles(): string {
             background: transparent !important;
             background-color: transparent !important;
         }
+        .lj-line {
+            display: block;
+            padding-left: 2ch;
+            text-indent: -2ch;
+        }
+        .lj-line-branch {
+            padding-left: 4ch;
+        }
         .lj-token-keyword {
             color: var(--lj-token-keyword);
         }
@@ -479,7 +487,7 @@ export function getStyles(): string {
             gap: 0.25rem;
         }
         .counterexample-line {
-            overflow-wrap: anywhere;
+            overflow-wrap: break-word;
         }
         .vc-line {
             display: contents;
@@ -488,7 +496,7 @@ export function getStyles(): string {
         .vc-predicate-cell {
             min-width: 0;
             padding: 0.0625rem 0.25rem;
-            overflow-wrap: anywhere;
+            overflow-wrap: break-word;
         }
         .vc-binder-cell {
             min-height: 1.2em;
@@ -499,6 +507,23 @@ export function getStyles(): string {
         .vc-predicate-cell {
             color: var(--vscode-editor-foreground);
         }
+        /* a narrow panel puts each binder above its predicate, so that the predicate gets the whole width */
+        @media (max-width: 420px) {
+            .diagnostic-item {
+                padding-inline: 0.5rem;
+            }
+            .vc-container {
+                padding-inline: 0.25rem;
+            }
+            .vc-chain {
+                grid-template-columns: minmax(0, 1fr);
+                line-height: 1.4;
+            }
+            .vc-binder-cell,
+            .vc-predicate-cell {
+                padding-inline: 0;
+            }
+        }
         .vc-arrow {
             font-size: 1.5em;
             line-height: 0;

client/src/webview/views/diagnostics/errors.ts

@@ -1,5 +1,6 @@
 import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton, renderHints } from "../sections";
 import { renderCounterexample } from "./counterexample";
+import { renderHighlightedLines } from "../../highlighting";
 import { renderVCImplication } from "./vc-implications";
 import type {
     ArgumentMismatchError,
@@ -38,14 +39,14 @@ type ErrorRendererMap = { [E in LJError as E['type']]: (error: E) => string };
 
 const errorContentRenderers: ErrorRendererMap = {
     'refinement-error': (e: RefinementError) => /*html*/ `
-        ${renderExpressionSection('Expected', e.expected)}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
         ${e.counterexample.assignments.length > 0
             ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample))
             : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/ `
-        ${renderExpressionSection('Expected', e.expected)}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
     `,
     'invalid-refinement-error': (e: InvalidRefinementError) => /*html*/ `

client/src/webview/views/diagnostics/vc-changes.spec.ts

@@ -25,7 +25,30 @@ describe('verification implications', () => {
         expect(document.querySelector('.vc-line:last-child')?.textContent?.trim()).toBe('x > 0');
         expect(Array.from(document.querySelectorAll('.vc-predicate-cell')).map(cell => cell.textContent?.trim()))
             .toEqual(['x == 1 →', 'y == 2 →', 'x > 0']);
-        expect(document.querySelectorAll('.vc-predicate-cell > .vc-arrow')).toHaveLength(2);
+        expect(document.querySelectorAll('.vc-predicate-cell .vc-arrow')).toHaveLength(2);
+    });
+    it('puts each top-level conjunct and each branch of a conditional on a line of its own', () => {
+        document.body.innerHTML = renderImplication({
+            name: 'h', type: 'Frame', predicate: 'a > 0 && (b || c) && s == "x && y"',
+            next: { ...conclusion, predicate: "p && q ? d(h) == on : (c == ':' ? d(h) == off : d(h) == on)" },
+        });
+
+        const lines = (cell: Element) => Array.from(cell.querySelectorAll('.lj-line'))
+            .map(line => [line.textContent, line.classList.contains('lj-line-branch')]);
+        const [fact, conditional] = document.querySelectorAll('.vc-predicate-cell');
+        expect(lines(fact)).toEqual([['a > 0 &&', false], ['(b || c) &&', false], ['s == "x && y" →', false]]);
+        expect(lines(conditional)).toEqual([
+            ['p && q', false], ['? d(h) == on', true], [": (c == ':' ? d(h) == off : d(h) == on)", true],
+        ]);
+    });
+    it('keeps a conjunct per line in a predicate that a simplification changed, marking a repeated conjunct it adds', () => {
+        document.body.innerHTML = renderImplicationChange(
+            { ...conclusion, predicate: 'x > 0' }, { ...conclusion, predicate: 'x > 0 && x > 0' },
+        );
+
+        expect(Array.from(document.querySelectorAll('.lj-line')).map(line => line.textContent)).toEqual(['x > 0 &&', 'x > 0']);
+        expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.textContent))
+            .toEqual(['x > 0 &&']);
     });
     it.each([
         ['initial rendering', () => renderImplication({ ...implication, next: null })],

client/src/webview/views/diagnostics/vc-changes.ts

@@ -1,6 +1,6 @@
 import type { VCImplication } from "../../../types/vc-implications";
 import type { TranslationTable } from "../../../types/diagnostics";
-import { renderHighlightedInlineExpression } from "../../highlighting";
+import { getExpressionLines, renderExpressionLines, renderHighlightedInlineExpression } from "../../highlighting";
 import { escapeHtml } from "../../utils";
 import { renderSourceHighlightButton } from "../sections";
 
@@ -49,17 +49,22 @@ function renderBinder(binder: string, type: string, translationTable?: Translati
     );
 }
 
+/**
+ * Renders a line of a VC chain, its predicate on the lines of getExpressionLines
+ * @param renderText renders the text of the line at an index, highlighted by default
+ */
 export function renderVCLine(
     line: string,
     className = "",
-    predicateContent?: string,
+    renderText?: (text: string, index: number) => string,
     translationTable?: TranslationTable,
 ): string {
     const { binder, type, predicate, hasNext } = parseImplicationLine(line);
+    const arrow = hasNext ? ' <span class="vc-arrow">→</span>' : "";
     return /*html*/`
         <div class="vc-line ${className}">
             ${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>${hasNext ? ' <span class="vc-arrow">→</span>' : ""}</div>
+            <div class="vc-predicate-cell"><span class="vc-node">${renderExpressionLines(getExpressionLines(predicate), renderText, arrow)}</span></div>
         </div>
     `;
 }
@@ -188,6 +193,18 @@ function alignChangedLines(removed: string[], added: string[]): Array<[string |
     return lines;
 }
 
+// each line of a changed predicate, diffed against the line of the old predicate it replaces, or all marked if none
+function renderChangedPredicateLines(before: string, after: string): string[] {
+    const lines = (predicate: string) => getExpressionLines(predicate).map(line => line.text);
+    return alignChangedLines(lines(before), lines(after))
+        .flatMap(([beforeLine, afterLine]) => {
+            if (afterLine === undefined) return [];
+            return [beforeLine === undefined
+                ? renderChangedFragment(afterLine)
+                : renderDestinationTokenDiff(beforeLine, afterLine).content];
+        });
+}
+
 function renderChangedDestinationLines(
     removed: string[],
     added: string[],
@@ -199,14 +216,14 @@ function renderChangedDestinationLines(
         .map(([before, after]) => {
             if (after === undefined) return "";
             if (before === undefined) return renderVCLine(after, "vc-change-line", undefined, translationTable);
-            const change = renderDestinationTokenDiff(
-                parseImplicationLine(before).predicate,
-                parseImplicationLine(after).predicate,
-            );
+            const beforePredicate = parseImplicationLine(before).predicate;
+            const afterPredicate = parseImplicationLine(after).predicate;
+            const change = renderDestinationTokenDiff(beforePredicate, afterPredicate);
+            const lines = renderChangedPredicateLines(beforePredicate, afterPredicate);
             return renderVCLine(
                 after,
                 change.hasAddedContent ? "" : "vc-change-line",
-                change.content,
+                (_text, index) => lines[index],
                 translationTable,
             );
         })