diff --git a/client/src/types/vc-implications.ts b/client/src/types/vc-implications.ts index 2ecc53a..a6750ed 100644 --- a/client/src/types/vc-implications.ts +++ b/client/src/types/vc-implications.ts @@ -8,4 +8,5 @@ export type VCImplication = { export type VCSimplificationResult = { implication: VCImplication; origin: VCSimplificationResult | null; + simplification: string | null; } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index fe9ee25..b8e6478 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -324,13 +324,43 @@ export function getStyles(): string { } .vc-container { display: flex; - justify-content: space-between; - align-items: flex-start; - gap: 1rem; + flex-direction: column; + gap: 0.375rem; margin: 0.5rem 0; } + .vc-step-header { + display: flex; + align-items: center; + justify-content: space-between; + gap: 0.75rem; + min-width: 0; + padding-bottom: 0.25rem; + border-bottom: 1px solid var(--vscode-widget-border, var(--vscode-panel-border)); + font-family: var(--vscode-font-family); + font-size: 0.8rem; + line-height: 1.25rem; + } + .vc-step-name { + min-width: 0; + overflow: hidden; + color: var(--vscode-descriptionForeground); + font-weight: 600; + text-overflow: ellipsis; + white-space: nowrap; + } + .vc-step-navigation { + display: inline-flex; + align-items: center; + gap: 0.25rem; + flex-shrink: 0; + } + .vc-step-position { + min-width: 2.5rem; + color: var(--vscode-descriptionForeground); + font-variant-numeric: tabular-nums; + text-align: right; + } .vc-chain { - flex: 1; display: flex; flex-direction: column; gap: 0.25rem; diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts index 848220b..2506c06 100644 --- a/client/src/webview/views/diagnostics/vc-implications.ts +++ b/client/src/webview/views/diagnostics/vc-implications.ts @@ -28,6 +28,32 @@ function renderStepButton(errorId: string, step: "previous" | "next", disabled: return ``; } +function renderStepHeader( + errorId: string, + current: VCSimplificationResult, + index: number, + stepCount: number, +): string { + const chronologicalStep = stepCount - index; + const simplification = current.simplification?.trim(); + const label = simplification || "Original"; + + return /*html*/` +
+ ${escapeHtml(label)} +
+ + ${chronologicalStep}/${stepCount} + +
+ ${renderStepButton(errorId, "previous", index === stepCount - 1)} + ${renderStepButton(errorId, "next", index === 0)} +
+
+
+ `; +} + export function handleVCImplicationStepClick(target: Element): boolean { const errorId = target.getAttribute("data-error-id"); const step = target.getAttribute("data-vc-step"); @@ -53,21 +79,19 @@ export function renderVCImplication( error.title, error.message ])); - const history: VCSimplificationResult[] = []; + const steps: VCSimplificationResult[] = []; for (let current: VCSimplificationResult | null = result; current; current = current.origin) { - history.push(current); + steps.push(current); } - const index = Math.min(stepIndexes.get(errorId) ?? 0, history.length - 1); + const index = Math.min(stepIndexes.get(errorId) ?? 0, steps.length - 1); stepIndexes.set(errorId, index); + const current = steps[index]; return /*html*/ `
-
${renderImplication(history[index].implication)}
-
- ${renderStepButton(errorId, "previous", index === history.length - 1)} - ${renderStepButton(errorId, "next", index === 0)} -
+ ${steps.length > 1 ? renderStepHeader(errorId, current, index, steps.length) : ""} +
${renderImplication(current.implication)}
`; } diff --git a/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java index 155c3ac..0dc9d26 100644 --- a/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java +++ b/server/src/main/java/dtos/diagnostics/VCSimplificationResultDTO.java @@ -5,7 +5,7 @@ /** * DTO for serializing a simplified VC and its complete predecessor states. */ -public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin) { +public record VCSimplificationResultDTO(VCImplicationDTO implication, VCSimplificationResultDTO origin, String simplification) { public static VCSimplificationResultDTO from(VCSimplificationResult result) { if (result == null) @@ -13,6 +13,8 @@ public static VCSimplificationResultDTO from(VCSimplificationResult result) { return new VCSimplificationResultDTO( VCImplicationDTO.from(result.getImplication()), - from(result.getOrigin())); + from(result.getOrigin()), + result.getSimplification() + ); } }