diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts
index db72b56..9b6b378 100644
--- a/client/src/types/diagnostics.ts
+++ b/client/src/types/diagnostics.ts
@@ -74,8 +74,8 @@ export type StateRefinementError = BaseDiagnostic & {
category: 'error';
type: 'state-refinement-error';
translationTable: TranslationTable;
- expected: string;
- found: string;
+ expected: ValDerivationNode;
+ found: ValDerivationNode;
customMessage: string;
}
diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts
index d75b6e4..ac4d62d 100644
--- a/client/src/webview/views/context/variables.ts
+++ b/client/src/webview/views/context/variables.ts
@@ -5,7 +5,7 @@ import { escapeHtml } from "../../utils";
import { renderToggleSection, renderHighlightButton, renderDiagnosticRevealButton } from "../sections";
export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string {
- const expected = errorAtCursor ? errorAtCursor.type == "refinement-error" ? errorAtCursor.expected.value : errorAtCursor.expected : undefined;
+ const expected = errorAtCursor ? errorAtCursor.expected.value : undefined;
return /*html*/`
${renderToggleSection('Variables', 'context-vars', isExpanded)}
diff --git a/client/src/webview/views/diagnostics/derivation-nodes.ts b/client/src/webview/views/diagnostics/derivation-nodes.ts
index 9948905..ca8e8a3 100644
--- a/client/src/webview/views/diagnostics/derivation-nodes.ts
+++ b/client/src/webview/views/diagnostics/derivation-nodes.ts
@@ -1,4 +1,4 @@
-import type { LJError, RefinementError } from "../../../types/diagnostics";
+import type { LJError, RefinementMismatchError } from "../../../types/diagnostics";
import type { DerivationNode, ValDerivationNode } from "../../../types/derivation-nodes";
import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../../highlighting";
import { escapeHtml } from "../../utils";
@@ -19,7 +19,7 @@ function renderToken(token: string): string {
}
function renderJsonTree(
- error: RefinementError,
+ error: RefinementMismatchError,
node: DerivationNode | undefined,
errorId: string,
path: string,
@@ -123,10 +123,11 @@ export function handleDerivationResetClick(target?: any): boolean {
}
export function renderDerivationNode(
- error: RefinementError,
+ error: RefinementMismatchError,
node: ValDerivationNode,
scope: "expected" | "found"
): string {
+ if (!node || typeof node !== "object" || !("value" in node)) return renderHighlightedExpression(String(node)); // primitive value without derivation
if (!node.origin) return renderHighlightedExpression(String(node.value)); // no derivation available
const errorId = hashError(error, scope);
diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts
index 010f949..f8a88ff 100644
--- a/client/src/webview/views/diagnostics/errors.ts
+++ b/client/src/webview/views/diagnostics/errors.ts
@@ -36,8 +36,8 @@ const errorContentRenderers: Partial
${e.counterexample ? renderExpressionSection('Counterexample', e.counterexample) : ''}
`,
'state-refinement-error': (e: StateRefinementError) => /*html*/`
- ${renderExpressionSection('Expected', e.expected)}
- ${renderExpressionSection('Found', e.found)}
+ ${renderCustomSection('Expected', renderDerivationNode(e, e.expected, 'expected'))}
+ ${renderCustomSection('Found', renderDerivationNode(e, e.found, 'found'))}
`,
'invalid-refinement-error': (e: InvalidRefinementError) => /*html*/`
${renderExpressionSection('Refinement', e.refinement)}
diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java
index 5bcd7c7..efcf369 100644
--- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java
+++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java
@@ -3,12 +3,13 @@
import dtos.diagnostics.SourcePositionDTO;
import dtos.diagnostics.TranslationTableDTO;
import liquidjava.diagnostics.errors.StateRefinementError;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
/**
* DTO for serializing StateRefinementError instances to JSON
*/
public record StateRefinementErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position,
- TranslationTableDTO translationTable, String expected, String found, String customMessage) {
+ TranslationTableDTO translationTable, ValDerivationNode expected, ValDerivationNode found, String customMessage) {
public static StateRefinementErrorDTO from(StateRefinementError error) {
return new StateRefinementErrorDTO("error", "state-refinement-error", error.getTitle(), error.getMessage(), error.getFile(),