[CatarinaGamboa]

Closes #187

What changes

The Verification panel's Expected box and every Found line:

• One line per top-level conjunct, with && at the end of each line except the last. An && inside parentheses or a string literal stays on its line. Nothing is split when a weaker operator (||, -->, ?:) sits outside the parentheses, so a line never looks like a conjunct of the whole expression.
• A conditional outside parentheses shows its condition on one line and each branch on an indented line of its own (? …, : …). This is what makes A1_09 fit.
• Wrapped lines have a hanging indent, so you can see where each line starts.
• No breaks inside names. The VC cells used overflow-wrap: anywhere, which gave failures.siz|e(), compressionN|otExplicit and display(host|) ==. They now use break-word, so a line breaks at a space and splits a name only when the name alone is wider than the line.
• Narrow panel (webview at most 420 px wide). Each binder (∀host) goes above its predicate, so the predicate gets the whole width. The card and the Found box get less horizontal padding, and the Found lines get line-height 1.4 instead of 1.6.

This is display only. The text of every expression is the same as before, only laid out on more lines. The hover and the CLI do not change.

Acceptance check: the six study tasks at the study width

Headless VS Code at 1600×900, Dark Modern, default side bar (300 px; the error card is about 240 px). Verifier 0.0.37, the released one, which is what this branch builds with. Each image shows main on the left and this PR on the right. The webview is 794 px tall. "Found ends at" is the bottom of the Found box, in webview px.

Task	Found ends at (main → PR)
A2_10	503 → 453
A1_38	575 → 544
A1_01	562 → 521
A2_04	413 → 414
A1_56	498 → 473
A1_09	996 → 740: on main it ran below the fold

Expected and Found are fully visible in all six, with no name broken.

A1_09	A1_01

A2_10	A1_38

A2_04	A1_56

Verifier version

None needed. This works with 0.0.37 and with main.

Overlap with open PRs

• List Found as facts and show only readable simplification steps #185 (Found as facts) may conflict. It splits each Found node into conjunct lines in vc-changes.ts (formatImplicationLines, with its own splitConjuncts), and this PR changes renderVCLine in the same file.
  • The two are compatible: this PR's split keeps a trailing &&, so a line List Found as facts and show only readable simplification steps #185 has already split is left as it is.
  • Whichever lands second should keep one splitConjuncts. This PR's copy is in highlighting.ts and follows the same rules.
  • List Found as facts and show only readable simplification steps #185's binder-hiding on continuation lines works with the stacked binder layout.
• Show the Context tab's refinements as the error messages show them #186 (Context tab): no overlap. This PR does not touch the Context tab or sections.ts.

Not changed

• The Locations links (file names such as E_OSS_A1_01_SlideRecode|r.java) still break anywhere. They are in a <pre> with break-word, and the names are wider than the card. This was outside the issue.
• Top-level || (A1_01's Expected) is not split into lines. The issue asks for conjuncts.

Checks

npm run test:unit (127 passed; 3 new tests, each fails on main), npm run test:typecheck, npm run lint, server mvn -B test (39 passed, unchanged).

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review

I audited this diff with the clean-code-principles checklist.

Fixed

• highlighting.ts: splitConjuncts and getExpressionLines were exported but are only used inside the module, so they are module-private now (encapsulation, YAGNI).
• renderHighlightedLines: the join("</span>") trick that closed spans is gone. Each line is now built explicitly, with the trailing arrow on the last line (KISS).

Declined

• DRY with List Found as facts and show only readable simplification steps #185's splitConjuncts in vc-changes.ts. Both PRs are open, so the duplicate goes away when the second one lands, with one copy kept (noted in the body).
• renderVCLine has two branches that both wrap in <span class="vc-node">. Merging them would move the arrow inside the animated diff highlight of changed lines, which would change how those look.
• The 420px breakpoint is a literal, as the other breakpoints in styles.ts are. A CSS comment says what it is for.

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main:

• [P2] Exclude character literals when locating conditional operators (highlighting.ts). In flag ? c == ':' : d, the colon inside ':' was taken for the conditional's separator.
• [P2] Apply line formatting to changed VC predicates (vc-changes.ts). After stepping through the simplifications, a predicate that a step changed was rendered from its diff-highlighted HTML on one line, bypassing the line split.

Fixed (both)

• topLevelIndices now skips single-quoted literals, with escapes, as well as strings. The existing line-split test covers it with c == ':'.
• renderVCLine now takes a function that renders the text of each line, instead of finished HTML. A changed predicate is split into lines first, and each line is diffed against the old predicate. Whether the line counts as changed is decided on the whole predicate, as before. The two branches of renderVCLine are now one, which also clears the clean-code point I had declined. New test: keeps a conjunct per line in a predicate that a simplification changed.

Tests: 127 unit, typecheck, lint, and 39 server tests pass.

[CatarinaGamboa]

Codex review, round 2

• [P2] Preserve change highlighting for repeated conjuncts (vc-changes.ts). Each line was diffed against the whole previous predicate. So for x > 0 becoming x > 0 && x > 0, the added x > 0 was not highlighted, because its tokens matched the old predicate.

Fixed. A changed predicate is now split into lines on both sides. The old and new lines are paired with the same alignChangedLines that pairs the lines of the chain. Each new line is diffed against the old line it replaces, and a new line that replaces none is highlighted whole. The test …marking a repeated conjunct it adds uses Codex's example and fails on round 1's code.

Tests: 127 unit, typecheck, lint, and 39 server tests pass.

[CatarinaGamboa]

Codex review, round 3

codex exec review --base origin/main: "I found no actionable regression in the changed code. The relevant unit tests pass."

The loop ends here: nothing to fix.