Skip to content

Commit 291ed4d

Browse files
authored
Fix Independent Derivation Expansion (#69)
1 parent c9d86f0 commit 291ed4d

File tree

2 files changed

+10
-6
lines changed

2 files changed

+10
-6
lines changed

client/src/webview/views/diagnostics/derivation-nodes.ts

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,8 @@ function renderJsonTree(
7777
return `<span class="node-value">${JSON.stringify(node)}</span>`;
7878
}
7979

80-
function hashError(error: LJError): string {
81-
const content = `${error.title}|${error.message}|${error.file}|${error.position?.lineStart ?? 0}`;
80+
function hashError(error: LJError, scope: string): string {
81+
const content = `${error.title}|${error.message}|${error.file}|${error.position?.lineStart ?? 0}|${scope}`;
8282
let hash = 0;
8383
for (let i = 0; i < content.length; i++) {
8484
const char = content.charCodeAt(i);
@@ -114,10 +114,14 @@ export function handleDerivationResetClick(target?: any): boolean {
114114
return false;
115115
}
116116

117-
export function renderDerivationNode(error: RefinementError, node: ValDerivationNode): string {
117+
export function renderDerivationNode(
118+
error: RefinementError,
119+
node: ValDerivationNode,
120+
scope: "expected" | "found"
121+
): string {
118122
if (!node.origin) return `<pre>${node.value}</pre>`; // no derivation available
119123

120-
const errorId = hashError(error);
124+
const errorId = hashError(error, scope);
121125
const expansions = getExpansions(errorId);
122126
return /*html*/ `
123127
<div class="container derivation-container" data-error-id="${errorId}">

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,8 @@ export function renderErrors(errors: LJError[], expandedErrors: Set<number>): st
3131
const errorContentRenderers: Partial<Record<LJError['type'], (error: LJError) => string>> = {
3232
'refinement-error': (e: RefinementError) => /*html*/`
3333
${e.customMessage ? renderSection('Message', e.customMessage) : ''}
34-
${renderCustomSection('Expected', renderDerivationNode(e, e.expected))}
35-
${renderCustomSection('Found', renderDerivationNode(e, e.found))}
34+
${renderCustomSection('Expected', renderDerivationNode(e, e.expected, 'expected'))}
35+
${renderCustomSection('Found', renderDerivationNode(e, e.found, 'found'))}
3636
${e.counterexample ? renderSection('Counterexample', e.counterexample) : ''}
3737
`,
3838
'state-refinement-error': (e: StateRefinementError) => /*html*/`

0 commit comments

Comments
 (0)