diff --git a/client/.vscode/launch.json b/client/.vscode/launch.json
index 9b05b66..6d500f0 100644
--- a/client/.vscode/launch.json
+++ b/client/.vscode/launch.json
@@ -12,9 +12,6 @@
             ],
             "stopOnEntry": false,
             "sourceMaps": true,
-            "outFiles": [
-                "${workspaceRoot}/out/src/**/*.js"
-            ],
             "preLaunchTask": "npm: watch"
         },
         {
diff --git a/client/src/lsp/client.ts b/client/src/lsp/client.ts
index 7ffbf69..4cadccc 100644
--- a/client/src/lsp/client.ts
+++ b/client/src/lsp/client.ts
@@ -6,8 +6,8 @@ import { updateStatusBar } from '../services/status-bar';
 import { handleLJDiagnostics } from '../services/diagnostics';
 import { onActiveFileChange } from '../services/events';
 import type { LJDiagnostic } from "../types/diagnostics";
-import { ContextHistory } from '../types/context';
-import { handleContextHistory } from '../services/context';
+import { LJContext } from '../types/context';
+import { handleContext } from '../services/context';
 
 /**
  * Starts the client and connects it to the language server
@@ -44,8 +44,8 @@ export async function runClient(context: vscode.ExtensionContext, port: number)
             handleLJDiagnostics(diagnostics);
         });
 
-        extension.client.onNotification("liquidjava/context", (contextHistory: ContextHistory) => {
-            handleContextHistory(contextHistory);
+        extension.client.onNotification("liquidjava/context", (context: LJContext) => {
+            handleContext(context);
         });
 
         const editor = vscode.window.activeTextEditor;
diff --git a/client/src/lsp/server.ts b/client/src/lsp/server.ts
index 96ed551..5805f45 100644
--- a/client/src/lsp/server.ts
+++ b/client/src/lsp/server.ts
@@ -1,7 +1,7 @@
 import * as vscode from 'vscode';
 import * as child_process from 'child_process';
 import * as path from 'path';
-import { getAvailablePort, killProcess } from '../utils/utils';
+import { getAvailablePort, killProcess, normalizeFilePath } from '../utils/utils';
 import { extension } from '../state';
 import { DEBUG_MODE, DEBUG_PORT, SERVER_JAR } from '../utils/constants';
 
@@ -22,7 +22,7 @@ export async function runLanguageServer(context: vscode.ExtensionContext, javaEx
     const jarPath = path.resolve(context.extensionPath, "dist", "server", SERVER_JAR);
     const args = ["-jar", jarPath, port.toString()];
     const options = {
-        cwd: vscode.workspace.workspaceFolders[0].uri.fsPath, // root path
+        cwd: normalizeFilePath(vscode.workspace.workspaceFolders[0].uri.fsPath), // root path
     };
     extension.logger.client.info("Creating language server process...");
     extension.serverProcess = child_process.spawn(javaExecutablePath, args, options);
diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts
index 1b3d0d1..8eb4b4d 100644
--- a/client/src/services/autocomplete.ts
+++ b/client/src/services/autocomplete.ts
@@ -1,9 +1,9 @@
 import * as vscode from "vscode";
 import { extension } from "../state";
-import type { Variable, ContextHistory, Ghost, Alias } from "../types/context";
+import type { LJVariable, LJContext, LJGhost, LJAlias } from "../types/context";
 import { getSimpleName } from "../utils/utils";
-import { getVariablesInScope } from "./context";
 import { LIQUIDJAVA_ANNOTATION_START, LJAnnotation } from "../utils/constants";
+import { filterDuplicateVariables, filterInstanceVariables } from "./context";
 
 type CompletionItemOptions = {
     name: string;
@@ -19,20 +19,20 @@ type CompletionItemOptions = {
 type CompletionItemKind = "vars" | "ghosts" | "aliases" | "keywords" | "types" | "decls" | "packages";
 
 /**
- * Registers a completion provider for LiquidJava annotations, providing context-aware suggestions based on the current context history
+ * Registers a completion provider for LiquidJava annotations, providing context-aware suggestions based on the current context
  */
 export function registerAutocomplete(context: vscode.ExtensionContext) {
     context.subscriptions.push(
         vscode.languages.registerCompletionItemProvider("java", {
             provideCompletionItems(document, position, _token, completionContext) {
                 const annotation = getActiveLiquidJavaAnnotation(document, position);
-                if (!annotation || !extension.contextHistory) return null;
+                if (!annotation || !extension.context) return null;
 
                 const isDotTrigger =  completionContext.triggerKind === vscode.CompletionTriggerKind.TriggerCharacter && completionContext.triggerCharacter === ".";
                 const receiver = isDotTrigger ? getReceiverBeforeDot(document, position) : null; 
                 const file = document.uri.toString().replace("file://", "");
                 const nextChar = document.getText(new vscode.Range(position, position.translate(0, 1)));
-                const items = getContextCompletionItems(extension.contextHistory, file, annotation, nextChar, isDotTrigger, receiver);
+                const items = getContextCompletionItems(extension.context, file, annotation, nextChar, isDotTrigger, receiver);
                 const uniqueItems = new Map<string, vscode.CompletionItem>();
                 items.forEach(item => {
                     const label = typeof item.label === "string" ? item.label : item.label.label;
@@ -44,19 +44,20 @@ export function registerAutocomplete(context: vscode.ExtensionContext) {
     );
 }
 
-function getContextCompletionItems(context: ContextHistory, file: string, annotation: LJAnnotation, nextChar: string, isDotTrigger: boolean, receiver: string | null): vscode.CompletionItem[] {
+function getContextCompletionItems(context: LJContext, file: string, annotation: LJAnnotation, nextChar: string, isDotTrigger: boolean, receiver: string | null): vscode.CompletionItem[] {
     const triggerParameterHints = nextChar !== "(";
+    const ghosts = context.ghosts.filter(ghost => ghost.file === file);
     if (isDotTrigger) {
         if (receiver === "this" || receiver === "old(this)") {
-            return getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints);
+            return getGhostCompletionItems(ghosts, triggerParameterHints);
         }
         return [];
-    } 
-    const variablesInScope = getVariablesInScope(file, extension.selection);
-    const inScope = variablesInScope !== null;
+    }
+    const inScope = extension.context.visibleVars !== null;
+    const varsInScope = filterDuplicateVariables(filterInstanceVariables([...context.visibleVars || []]));
     const itemsHandlers: Record<CompletionItemKind, () => vscode.CompletionItem[]> = {
-        vars: () => getVariableCompletionItems(variablesInScope || []),
-        ghosts: () => getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints),
+        vars: () => getVariableCompletionItems(varsInScope),
+        ghosts: () => getGhostCompletionItems(ghosts, triggerParameterHints),
         aliases: () => getAliasCompletionItems(context.aliases, triggerParameterHints),
         keywords: () => getKeywordsCompletionItems(triggerParameterHints, inScope),
         types: () => getTypesCompletionItems(),
@@ -75,7 +76,7 @@ function getContextCompletionItems(context: ContextHistory, file: string, annota
     return itemsMap[annotation].map(key => itemsHandlers[key]()).flat();
 }
 
-function getVariableCompletionItems(variables: Variable[]): vscode.CompletionItem[] {
+function getVariableCompletionItems(variables: LJVariable[]): vscode.CompletionItem[] {
     return variables.map(variable => {
         const varSig = `${variable.type} ${variable.name}`;
         const codeBlocks: string[] = [];
@@ -91,12 +92,11 @@ function getVariableCompletionItems(variables: Variable[]): vscode.CompletionIte
     });
 }
 
-function getGhostCompletionItems(ghosts: Ghost[], triggerParameterHints: boolean): vscode.CompletionItem[] {
+function getGhostCompletionItems(ghosts: LJGhost[], triggerParameterHints: boolean): vscode.CompletionItem[] {
     return ghosts.map(ghost => {
         const parameters = ghost.parameterTypes.map(getSimpleName).join(", ");
         const ghostSig = `${ghost.returnType} ${ghost.name}(${parameters})`;
-        const isState = /^state\d+\(_\) == \d+$/.test(ghost.refinement);
-        const description = isState ? "state" : "ghost";
+        const description = ghost.isState ? "state" : "ghost";
         return createCompletionItem({
             name: ghost.name,
             kind: vscode.CompletionItemKind.Function,
@@ -110,7 +110,7 @@ function getGhostCompletionItems(ghosts: Ghost[], triggerParameterHints: boolean
     });
 }
 
-function getAliasCompletionItems(aliases: Alias[], triggerParameterHints: boolean): vscode.CompletionItem[] {
+function getAliasCompletionItems(aliases: LJAlias[], triggerParameterHints: boolean): vscode.CompletionItem[] {
     return aliases.map(alias => {
         const parameters = alias.parameters
             .map((parameter, index) => {
diff --git a/client/src/services/context.ts b/client/src/services/context.ts
index e481f42..47efe77 100644
--- a/client/src/services/context.ts
+++ b/client/src/services/context.ts
@@ -1,65 +1,149 @@
 import { extension } from "../state";
-import { ContextHistory, Selection, Variable } from "../types/context";
+import { LJContext, Range, LJVariable } from "../types/context";
+import { SourcePosition } from "../types/diagnostics";
+import { getOriginalVariableName } from "../utils/utils";
 
-export function handleContextHistory(contextHistory: ContextHistory) {
-    extension.contextHistory = contextHistory;
+export function handleContext(context: LJContext) {
+    extension.context = context;
+    updateContextForSelection(extension.currentSelection);
+    extension.webview.sendMessage({ type: "context", context: extension.context });
 }
 
-// Gets the variables in scope for a given file and position
-// Returns null if position not in any scope
-export function getVariablesInScope(file: string, selection: Selection): Variable[] | null {
-    if (!extension.contextHistory || !selection || !file) return null;
+export function updateContextForSelection(selection: Range) {
+    if (!selection) return;
 
-    // get variables in file
-    const fileVars = extension.contextHistory.vars[file];
-    if (!fileVars) return null;
+    const globalVars = extension.context.globalVars || [];
+    const localVars = extension.context.localVars || [];
+    const scope = getMostSpecificScope(extension.file, selection);
 
-    // get variables in the current scope based on the selection
-    let mostSpecificScope: string | null = null;
-    let minScopeSize = Infinity;
+    let visibleVars: LJVariable[] = [];
+    if (scope) {
+        const variablesInScope = getVariablesInScope(localVars, extension.file, scope);
+        visibleVars = getVisibleVariables(variablesInScope, extension.file, selection);
+    }
+
+    const allVars = sortVariables(normalizeVariableRefinements([...globalVars, ...visibleVars]));
+    extension.context.visibleVars = visibleVars;
+    extension.context.allVars = allVars;
+}
 
-    // find the most specific scope that contains the selection
-    for (const scope of Object.keys(fileVars)) {
-        const scopeSelection = parseScopeString(scope);
-        if (isSelectionWithinScope(selection, scopeSelection)) {
-            const scopeSize = (scopeSelection.endLine - scopeSelection.startLine) * 10000 + (scopeSelection.endColumn - scopeSelection.startColumn);
+function getMostSpecificScope(file: string, range: Range): Range | null {
+    // get scopes for the current file
+    const scopes = extension.context.fileScopes[file];
+    if (!scopes) return null;
+    
+    // find the most specific scope that contains the range
+    let mostSpecificScope: Range | null = null;
+    let minScopeSize = Infinity;
+    for (const scope of scopes) {
+        if (isRangeWithin(range, scope)) {
+            const scopeSize = (scope.lineEnd - scope.lineStart) * 10000 + (scope.colEnd - scope.colStart);
             if (scopeSize < minScopeSize) {
                 mostSpecificScope = scope;
                 minScopeSize = scopeSize;
             }
         }
     }
-    if (mostSpecificScope === null)
-        return null;
+    return mostSpecificScope;
+}
+
+function getVariablesInScope(variables: LJVariable[], file: string, scope: Range): LJVariable[] {
+    return variables.filter(v => v.position?.file === file && isRangeWithin(v.position, scope));
+}
+
+function getVisibleVariables(variables: LJVariable[], file: string, selection: Range): LJVariable[] {
+    const isCollapsedRange = selection.lineStart === selection.lineEnd && selection.colStart === selection.colEnd;
+    const fileScopes = isCollapsedRange ? (extension.context.fileScopes[file] || []) : [];
+    return variables.filter((variable) => {
+        if (!variable.position) return false; // variable has no position
+        if (variable.position?.file !== file) return false; // variable is not in the current file
+       
+        // single point cursor
+        if (isCollapsedRange) {
+            const position: SourcePosition = variable.annotationPosition || variable.position!;
+            if (!position) return false;
+
+            // variable was declared before the cursor line or its in the same line but before the cursor column
+            const isDeclaredBeforeCursor =
+                position.lineStart < selection.lineStart ||
+                (position.lineStart === selection.lineStart && position.colStart + 1 <= selection.colStart);
+            if (!isDeclaredBeforeCursor) return false;
 
-    // filter variables to only include those that are reachable based on their position
-    const variablesInScope = fileVars[mostSpecificScope];
-    const reachableVariables = getReachableVariables(variablesInScope, selection);
-    return reachableVariables.filter(v => !v.name.startsWith("this#"));
+            // exclude variables that in unreachable scopes
+            const isInUnreachableScope = fileScopes.some(scope =>
+                isRangeWithin(variable.position!, scope) && !isRangeWithin(selection, scope)
+            );
+            return !isInUnreachableScope;
+        }
+        // normal range, filter variables that are only within the range
+        return isRangeWithin(variable.position, selection);
+    });
 }
 
-function parseScopeString(scope: string): Selection {
-    const [start, end] = scope.split("-");
-    const [startLine, startColumn] = start.split(":").map(Number);
-    const [endLine, endColumn] = end.split(":").map(Number);
-    return { startLine, startColumn, endLine, endColumn };
+// Normalizes the range to ensure start is before end
+export function normalizeRange(range: Range): Range {
+    const isStartBeforeEnd =
+        range.lineStart < range.lineEnd ||
+        (range.lineStart === range.lineEnd && range.colStart <= range.colEnd);
+
+    if (isStartBeforeEnd) return range;
+    return {
+        lineStart: range.lineEnd,
+        colStart: range.colEnd,
+        lineEnd: range.lineStart,
+        colEnd: range.colStart,
+    };
 }
 
-function isSelectionWithinScope(selection: Selection, scope: Selection): boolean {
-    const startsWithin = selection.startLine > scope.startLine || 
-        (selection.startLine === scope.startLine && selection.startColumn >= scope.startColumn);
-    const endsWithin = selection.endLine < scope.endLine || 
-        (selection.endLine === scope.endLine && selection.endColumn <= scope.endColumn);
+function isRangeWithin(range: Range, another: Range): boolean {
+    const startsWithin = range.lineStart > another.lineStart || 
+        (range.lineStart === another.lineStart && range.colStart >= another.colStart);
+    const endsWithin = range.lineEnd < another.lineEnd || 
+        (range.lineEnd === another.lineEnd && range.colEnd <= another.colEnd);
     return startsWithin && endsWithin;
 }
 
-function getReachableVariables(variables: Variable[], selection: Selection): Variable[] {
-    return variables.filter((variable) => {
-        const placement = variable.placementInCode?.position;
-        const startPosition = variable.annPosition || placement;
-        if (!startPosition || variable.isParameter) return true; // if is parameter we need to access it even if it's declared after the selection (for method and parameter refinements)
-        
-        // variable was declared before the cursor line or its in the same line but before the cursor column
-        return startPosition.line < selection.startLine || startPosition.line === selection.startLine && startPosition.column <= selection.startColumn;
+export function filterDuplicateVariables(variables: LJVariable[]): LJVariable[] {
+    const uniqueVariables: Map<string, LJVariable> = new Map();
+    for (const variable of variables) {
+        if (!uniqueVariables.has(variable.name)) {
+            uniqueVariables.set(variable.name, variable);
+        }
+    }
+    return Array.from(uniqueVariables.values());
+}
+
+function sortVariables(variables: LJVariable[]): LJVariable[] {
+    // sort by position or name
+    return variables.sort((left, right) => {
+        if (!left.position && !right.position) return compareVariableNames(left, right);
+        if (!left.position) return 1;
+        if (!right.position) return -1;
+        if (left.position.lineStart !== right.position.lineStart) return left.position.lineStart - right.position.lineStart;
+        if (left.position.colStart !== right.position.colStart) return right.position.colStart - left.position.colStart;
+        return compareVariableNames(left, right);
+    });
+}
+
+function compareVariableNames(a: LJVariable, b: LJVariable): number {
+    if (a.name.startsWith("#") && b.name.startsWith("#")) return getOriginalVariableName(a.name).localeCompare(getOriginalVariableName(b.name));
+    if (a.name.startsWith("#")) return 1;
+    if (b.name.startsWith("#")) return -1;
+    return a.name.localeCompare(b.name);
+}
+
+export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] {
+    return variables.filter(v => !v.name.includes("#"));
+}
+
+function normalizeVariableRefinements(variables: LJVariable[]): LJVariable[] {
+    return Array.from(new Map(variables.map(v => [v.refinement, v])).values()).flatMap(v => {
+        if (!v.refinement || v.refinement === "true") return []; // filter out trivial refinements
+        if (v.refinement.includes("==")) {
+            const [left, right] = v.refinement.split("==").map(s => s.trim());
+            return left !== right ? [v] : []; // filter tautologies like x == x
+        }
+        if (v.refinement.includes("!=")) return [v];
+        return [{ ...v, refinement: `${v.name} == ${v.refinement}` }];
     });
 }
\ No newline at end of file
diff --git a/client/src/services/diagnostics.ts b/client/src/services/diagnostics.ts
index e8a406d..a8164d2 100644
--- a/client/src/services/diagnostics.ts
+++ b/client/src/services/diagnostics.ts
@@ -11,8 +11,8 @@ export function handleLJDiagnostics(diagnostics: LJDiagnostic[]) {
     const containsError = diagnostics.some(d => d.category === "error");
     const statusBarState: StatusBarState = containsError ? "failed" : "passed";
     updateStatusBar(statusBarState);
-    extension.webview?.sendMessage({ type: "diagnostics", diagnostics });
     extension.diagnostics = diagnostics;
+    extension.webview?.sendMessage({ type: "diagnostics", diagnostics });
 }
 
 /**
diff --git a/client/src/services/editor.ts b/client/src/services/editor.ts
new file mode 100644
index 0000000..2b33557
--- /dev/null
+++ b/client/src/services/editor.ts
@@ -0,0 +1,30 @@
+import * as vscode from 'vscode'
+import { Range } from '../types/context';
+
+const highlight = vscode.window.createTextEditorDecorationType({
+    backgroundColor: 'rgba(255, 255, 0, 0.3)'
+})
+
+export async function openFile(filePath: string, line: number, character: number, rangeToHighlight?: Range) {
+    const uri = vscode.Uri.file(filePath);
+    const doc = await vscode.workspace.openTextDocument(uri);
+    const editor = await vscode.window.showTextDocument(doc);
+    const position = new vscode.Position(line, character);
+    const range = new vscode.Range(position, position);
+    editor.selection = new vscode.Selection(position, position);
+    editor.revealRange(range, vscode.TextEditorRevealType.InCenter);
+    if (rangeToHighlight) highlightRange(editor, rangeToHighlight);
+}
+
+export function highlightRange(editor: vscode.TextEditor, range: Range) {
+    if (!range) {
+        editor.setDecorations(highlight, []);
+        return;
+    }
+    const nativeRange = new vscode.Range(
+        new vscode.Position(range.lineStart, range.colStart),
+        new vscode.Position(range.lineEnd, range.colEnd)
+    )
+    editor.setDecorations(highlight, [{ range: nativeRange }])
+    editor.revealRange(nativeRange, vscode.TextEditorRevealType.InCenter)
+}
\ No newline at end of file
diff --git a/client/src/services/events.ts b/client/src/services/events.ts
index bc8501b..b471473 100644
--- a/client/src/services/events.ts
+++ b/client/src/services/events.ts
@@ -1,11 +1,12 @@
 import * as vscode from 'vscode';
 import { extension } from '../state';
 import { updateStateMachine } from './state-machine';
-import { Selection } from '../types/context';
 import { SELECTION_DEBOUNCE_MS } from '../utils/constants';
+import { normalizeRange, updateContextForSelection } from './context';
+import { normalizeFilePath } from '../utils/utils';
+import { Range } from '../types/context';
 
 let selectionTimeout: NodeJS.Timeout | null = null;
-let currentSelection: Selection = { startLine: 0, startColumn: 0, endLine: 0, endColumn: 0 };
 
 /**
  * Initializes file system event listeners
@@ -35,26 +36,38 @@ export function registerEvents(context: vscode.ExtensionContext) {
  * @param editor The active text editor
  */
 export async function onActiveFileChange(editor: vscode.TextEditor) {
-    extension.file = editor.document.uri.fsPath;
+    extension.file = normalizeFilePath(editor.document.uri.fsPath);
     extension.webview?.sendMessage({ type: "file", file: extension.file });
     await updateStateMachine(editor.document);
+    handleContextUpdate(editor.selection);
 }
 
 /**
  * Handles selection change events
  * @param event The selection change event
  */
-export async function onSelectionChange(event: vscode.TextEditorSelectionChangeEvent) {        
-    // update current selection
-    const selectionStart = event.selections[0].start;
-    const selectionEnd = event.selections[0].end;
-    currentSelection = {
-        startLine: selectionStart.line,
-        startColumn: selectionStart.character,
-        endLine: selectionEnd.line,
-        endColumn: selectionEnd.character
-    };
+export async function onSelectionChange(event: vscode.TextEditorSelectionChangeEvent) { 
     // debounce selection changes
     if (selectionTimeout) clearTimeout(selectionTimeout);
-    selectionTimeout = setTimeout(() => extension.selection = currentSelection, SELECTION_DEBOUNCE_MS);
+    selectionTimeout = setTimeout(() => {
+        handleContextUpdate(event.selections[0]);
+    }, SELECTION_DEBOUNCE_MS);
+}
+
+/**
+ * Updates the current selection and context
+ * @param selection The new selection
+ */
+function handleContextUpdate(selection: vscode.Selection) {
+    if (!extension.file || !extension.context) return;
+    const range: Range = {
+        lineStart: selection.start.line,
+        colStart: selection.start.character,
+        lineEnd: selection.end.line,
+        colEnd: selection.end.character
+    };
+    const normalizedRange = normalizeRange(range);
+    extension.currentSelection = normalizedRange;
+    updateContextForSelection(normalizedRange);
+    extension.webview?.sendMessage({ type: "context", context: extension.context });
 }
\ No newline at end of file
diff --git a/client/src/services/state-machine.ts b/client/src/services/state-machine.ts
index cfa7c26..34db194 100644
--- a/client/src/services/state-machine.ts
+++ b/client/src/services/state-machine.ts
@@ -1,13 +1,13 @@
 import * as vscode from "vscode";
 import { extension } from "../state";
-import { StateMachine } from "../types/fsm";
+import { LJStateMachine } from "../types/fsm";
 
 /**
  * Requests the state machine for the given document from the language server
  * @param document The text document
  */
 export async function updateStateMachine(document: vscode.TextDocument) {
-    const sm: StateMachine = await extension.client?.sendRequest("liquidjava/fsm", { uri: document.uri.toString() });
+    const sm: LJStateMachine = await extension.client?.sendRequest("liquidjava/fsm", { uri: document.uri.toString() });
     extension.webview?.sendMessage({ type: "fsm", sm });
     extension.stateMachine = sm;
 }
diff --git a/client/src/services/webview.ts b/client/src/services/webview.ts
index 6391677..e4d7dbe 100644
--- a/client/src/services/webview.ts
+++ b/client/src/services/webview.ts
@@ -22,10 +22,10 @@ export function registerWebview(context: vscode.ExtensionContext) {
     // listen for messages from the webview
     context.subscriptions.push(
         extension.webview.onDidReceiveMessage(message => {
-            console.log("received message", message);
             if (message.type === "ready") {
-                extension.webview.sendMessage({ type: "file", file: extension.file });
-                extension.webview.sendMessage({ type: "diagnostics", diagnostics: extension.diagnostics });
+                if (extension.file) extension.webview.sendMessage({ type: "file", file: extension.file });
+                if (extension.diagnostics) extension.webview.sendMessage({ type: "diagnostics", diagnostics: extension.diagnostics });
+                if (extension.context) extension.webview.sendMessage({ type: "context", context: extension.context });
                 if (extension.stateMachine) extension.webview.sendMessage({ type: "fsm", sm: extension.stateMachine });
             }
         })
diff --git a/client/src/state.ts b/client/src/state.ts
index 6b473c8..6e1736c 100644
--- a/client/src/state.ts
+++ b/client/src/state.ts
@@ -5,8 +5,8 @@ import { LanguageClient } from "vscode-languageclient/node";
 import { LiquidJavaLogger } from "./services/logger";
 import { LiquidJavaWebviewProvider } from "./webview/provider";
 import type { LJDiagnostic } from "./types/diagnostics";
-import type { StateMachine } from "./types/fsm";
-import { ContextHistory, Selection } from "./types/context";
+import type { LJStateMachine } from "./types/fsm";
+import { LJContext, Range } from "./types/context";
 
 export class ExtensionState {
     // server/client state
@@ -22,9 +22,9 @@ export class ExtensionState {
     // application state
     file?: string;
     diagnostics?: LJDiagnostic[];
-    stateMachine?: StateMachine;
-    contextHistory?: ContextHistory;
-    selection?: Selection;
+    stateMachine?: LJStateMachine;
+    context?: LJContext;
+    currentSelection?: Range;
 }
 
 export const extension = new ExtensionState();
\ No newline at end of file
diff --git a/client/src/types/context.ts b/client/src/types/context.ts
index 145a070..7943c9e 100644
--- a/client/src/types/context.ts
+++ b/client/src/types/context.ts
@@ -1,43 +1,46 @@
-import { PlacementInCode, SourcePosition } from "./diagnostics";
+import { SourcePosition } from "./diagnostics";
 
 // Type definitions used for LiquidJava context information
 
-export type Variable = {
+export type LJVariable = {
   name: string;
   type: string;
   refinement: string;
   mainRefinement: string;
-  placementInCode: PlacementInCode | null;
-  isParameter: boolean;
-  annPosition: SourcePosition | null;
+  position: SourcePosition| null;
+  annotationPosition: SourcePosition | null;
 }
 
-export type Ghost = {
+export type LJGhost = {
   name: string;
   qualifiedName: string;
   returnType: string;
   parameterTypes: string[];
   refinement: string;
+  isState: boolean;
+  file: string;
 }
 
-export type Alias = {
+export type LJAlias = {
   name: string;
   parameters: string[];
   types: string[];
   predicate: string;
 }
 
-export type ContextHistory = {
-  vars: Record<string, Record<string, Variable[]>>; // file -> (scope -> variables in scope)
-  ghosts: Record<string, Ghost[]>; // file -> ghosts in file
-  instanceVars: Variable[];
-  globalVars: Variable[];
-  aliases: Alias[];
+export type LJContext = {
+  localVars: LJVariable[];
+  globalVars: LJVariable[];
+  ghosts: LJGhost[];
+  aliases: LJAlias[];
+  visibleVars: LJVariable[]; // variables visible in the current selection
+  allVars: LJVariable[]; // instance vars + global vars + vars in scope
+  fileScopes: Record<string, Range[]>; // file -> scopes
 }
 
-export type Selection = {
-  startLine: number;
-  startColumn: number;
-  endLine: number;
-  endColumn: number;
+export type Range = {
+  lineStart: number;
+  colStart: number;
+  lineEnd: number;
+  colEnd: number;
 }
\ No newline at end of file
diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts
index 6c84af1..16ba427 100644
--- a/client/src/types/diagnostics.ts
+++ b/client/src/types/diagnostics.ts
@@ -1,23 +1,15 @@
 import type { ValDerivationNode } from './derivation-nodes';
+import type { Range } from './context';
 
 // Type definitions used for LiquidJava diagnostics
 
-export type ErrorPosition = {
-    lineStart: number;
-    lineEnd: number;
-    colStart: number;
-    colEnd: number;
-}
-
-export type SourcePosition = {
-    file: string;
-    line: number;
-    column: number;
+export type SourcePosition = Range & {
+    file: string | null;
 }
 
 export type PlacementInCode = {
     text: string;
-    position: SourcePosition;
+    position: SourcePosition | null;
 }
 
 export type TranslationTable = Record<string, PlacementInCode>;
@@ -34,7 +26,7 @@ type BaseDiagnostic = {
     title: string;
     message: string;
     file: string;
-    position?: ErrorPosition;
+    position: SourcePosition | null;
 }
 
 export type CustomError = BaseDiagnostic & {
diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts
index f7c726c..e8f1a96 100644
--- a/client/src/types/fsm.ts
+++ b/client/src/types/fsm.ts
@@ -1,6 +1,6 @@
 // Type definitions used for representing finite state machines
 
-export type StateMachine = {
+export type LJStateMachine = {
     className: string;
     initialStates: string[];
     states: string[];
diff --git a/client/src/utils/utils.ts b/client/src/utils/utils.ts
index e0eb229..14b233b 100644
--- a/client/src/utils/utils.ts
+++ b/client/src/utils/utils.ts
@@ -127,4 +127,13 @@ export async function killProcess(proc?: child_process.ChildProcess) {
 export function getSimpleName(qualifiedName: string): string {
     const parts = qualifiedName.split(".");
     return parts[parts.length - 1];
+}
+
+export function getOriginalVariableName(name: string): string {
+    return name.split("_")[0].replace(/^#/, '');
+}
+
+export function normalizeFilePath(fsPath: string): string {
+    // uppercase windows drive letter (c:\ -> C:\)
+    return path.normalize(fsPath).replace(/^([a-z]):\\/, (_, drive) => drive.toUpperCase() + ':\\');
 }
\ No newline at end of file
diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts
index 3878eee..168ed59 100644
--- a/client/src/webview/diagram.ts
+++ b/client/src/webview/diagram.ts
@@ -1,4 +1,4 @@
-import type { StateMachine } from "../types/fsm";
+import type { LJStateMachine } from "../types/fsm";
 
 // constants
 const MIN_ZOOM = 0.2;
@@ -21,7 +21,7 @@ let startY = 0;
  * @param sm 
  * @returns Mermaid diagram string
  */
-export function createMermaidDiagram(sm: StateMachine, orientation: "LR" | "TB"): string {
+export function createMermaidDiagram(sm: LJStateMachine, orientation: "LR" | "TB"): string {
     if (!sm) return '';
     
     const lines: string[] = [];
diff --git a/client/src/webview/provider.ts b/client/src/webview/provider.ts
index ddd4c0d..1cacfe9 100644
--- a/client/src/webview/provider.ts
+++ b/client/src/webview/provider.ts
@@ -1,5 +1,6 @@
 import * as vscode from 'vscode';
 import { getHtml } from './html';
+import { highlightRange, openFile } from '../services/editor';
 
 /**
  * Webview provider for the LiquidJava extension
@@ -32,18 +33,10 @@ export class LiquidJavaWebviewProvider implements vscode.WebviewViewProvider {
       
       // handle message
       if (message.type === "openFile") {
-        // open file at the specified location
-        const uri = vscode.Uri.file(message.filePath);
-        vscode.workspace.openTextDocument(uri).then(doc => {
-          vscode.window.showTextDocument(doc).then(editor => {
-            const line = message.line - 1;
-            const character = message.character - 1;
-            const position = new vscode.Position(line, character);
-            const range = new vscode.Range(position, position);
-            editor.selection = new vscode.Selection(position, position);
-            editor.revealRange(range, vscode.TextEditorRevealType.InCenter);
-          });
-        });
+        openFile(message.filePath, message.line, message.character, message.highlightRange);
+      } else if (message.type === "highlight") {
+        // highlight the specified range in the current editor
+        highlightRange(vscode.window.activeTextEditor, message.range);
       }
     });
   }
diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts
index dfa4ff8..1af0263 100644
--- a/client/src/webview/script.ts
+++ b/client/src/webview/script.ts
@@ -1,11 +1,14 @@
-import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/verification/derivation-nodes";
+import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/diagnostics/derivation-nodes";
 import { renderLoading } from "./views/loading";
-import { renderStateMachineView } from "./views/diagram";
-import { createMermaidDiagram, renderMermaidDiagram, resetZoom, registerPanListeners, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram";
+import { renderStateMachineView } from "./views/fsm/fsm";
+import { createMermaidDiagram, renderMermaidDiagram, resetZoom, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram";
 import type { LJDiagnostic } from "../types/diagnostics";
-import type { StateMachine } from "../types/fsm";
+import type { Range } from "../types/context";
+import type { LJStateMachine } from "../types/fsm";
 import type { NavTab } from "./views/sections";
-import { renderVerificationView } from "./views/verification/verification";
+import { renderDiagnosticsView } from "./views/diagnostics/diagnostics";
+import { LJContext } from "../types/context";
+import { ContextSectionState, renderContextView } from "./views/context/context";
 
 /**
  * Initializes the webview script
@@ -19,10 +22,16 @@ export function getScript(vscode: any, document: any, window: any) {
     let showAllDiagnostics = false;
     let currentFile: string | undefined;
     let expandedErrors = new Set<number>();
-    let stateMachine: StateMachine | undefined;
-    let selectedTab: NavTab = 'verification';
+    let stateMachine: LJStateMachine | undefined;
+    let context: LJContext | undefined;
+    let selectedTab: NavTab = 'diagnostics';
     let diagramOrientation: "LR" | "TB" = "TB";
     let currentDiagram: string = '';
+    const contextSectionState: ContextSectionState = {
+        aliases: false,
+        ghosts: false,
+        vars: true,
+    };
 
     // initial state
     root.innerHTML = renderLoading();
@@ -33,6 +42,34 @@ export function getScript(vscode: any, document: any, window: any) {
         const target = e.target as any;
         if (!target) return;
 
+        // context section toggle
+        const contextToggleButton = target.closest?.('.context-toggle-btn');
+        if (contextToggleButton) {
+            e.preventDefault();
+            e.stopPropagation();
+
+            const sectionId = contextToggleButton.getAttribute('data-context-toggle');
+            if (!sectionId) return;
+
+            const content = document.getElementById(sectionId);
+            if (!content) return;
+
+            const isExpanded = contextToggleButton.getAttribute('aria-expanded') !== 'false';
+            const nextExpanded = !isExpanded;
+            if (sectionId === 'context-vars') contextSectionState.vars = nextExpanded;
+            if (sectionId === 'context-ghosts') contextSectionState.ghosts = nextExpanded;
+            if (sectionId === 'context-aliases') contextSectionState.aliases = nextExpanded;
+            contextToggleButton.setAttribute('aria-expanded', nextExpanded ? 'true' : 'false');
+            content.classList.toggle('collapsed', !nextExpanded);
+
+            const icon = contextToggleButton.querySelector('.context-toggle-icon');
+            if (icon) {
+                icon.textContent = nextExpanded ? '▾' : '▸';
+            }
+
+            return;
+        }
+
         // location link or variable click
         if (target.classList.contains('location-link') || target.classList.contains('node-var')) {
             e.preventDefault();
@@ -131,11 +168,44 @@ export function getScript(vscode: any, document: any, window: any) {
             return;
         }
 
+        // highlight variable 
+        if (target.classList.contains('highlight-var-btn')) {
+            e.stopPropagation();
+
+            const previousSelected = root.querySelector('.highlight-var-btn.selected');        
+            if (previousSelected) {
+                // unselect previous
+                previousSelected.classList.remove('selected');
+                if (previousSelected === target) {
+                    // remove highlight
+                    vscode.postMessage({ type: 'highlight', range: null });
+                    return;
+                }
+            }
+            target.classList.add('selected');
+
+            const file = target.getAttribute('data-file');
+            const lineStart = parseInt(target.getAttribute('data-start-line') || '', 10);
+            const colStart = parseInt(target.getAttribute('data-start-column') || '', 10);
+            const lineEnd = parseInt(target.getAttribute('data-end-line') || '', 10);
+            const colEnd = parseInt(target.getAttribute('data-end-column') || '', 10);
+            if ([lineStart, colStart, lineEnd, colEnd].some(Number.isNaN)) return;
+
+            const range: Range = { lineStart, colStart, lineEnd, colEnd };
+            if (file !== currentFile) {
+                vscode.postMessage({ type: 'openFile', filePath: file, line: lineStart, character: colStart, highlightRange: range });
+            } else {
+                vscode.postMessage({ type: 'highlight', range })
+            }
+            return;
+        }
+
         // nav tab click
         if (target.classList.contains('nav-tab')) {
             e.stopPropagation();
             const tab = target.getAttribute('data-tab') as NavTab;
             if (tab && tab !== selectedTab) {
+                vscode.postMessage({ type: 'highlight', range: null });
                 selectedTab = tab;
                 updateView();
             }
@@ -146,20 +216,23 @@ export function getScript(vscode: any, document: any, window: any) {
     // message event listener from extension
     window.addEventListener('message', event => {
         const msg = event.data;
-        if (msg.type === 'diagnostics') {
-            diagnostics = msg.diagnostics as LJDiagnostic[];
-            updateView();
-        } else if (msg.type === 'file') {
-            currentFile = msg.file;
-            if (!showAllDiagnostics) updateView();
-        } else if (msg.type === 'fsm') {
-            if (!msg.sm) {
-                stateMachine = undefined;
-                updateView();
-                return;
-            }
-            stateMachine = msg.sm as StateMachine;
-            updateView();
+        switch (msg.type) {
+            case 'diagnostics':
+                diagnostics = msg.diagnostics as LJDiagnostic[];
+                if (selectedTab === 'diagnostics') updateView();
+                break;
+            case 'file':
+                currentFile = msg.file;
+                if (!showAllDiagnostics && selectedTab === 'diagnostics') updateView();
+                break;
+            case 'fsm':
+                stateMachine = msg.sm as LJStateMachine | undefined;
+                if (selectedTab === 'fsm') updateView();
+                break;
+            case 'context':
+                context = msg.context as LJContext;
+                if (selectedTab === 'context') updateView();
+                break;
         }
     });
 
@@ -167,13 +240,19 @@ export function getScript(vscode: any, document: any, window: any) {
      * Updates the webview content based on the current state
      */
     function updateView() {
-        if (selectedTab === 'verification') {
-            root.innerHTML = renderVerificationView(diagnostics, showAllDiagnostics, currentFile, expandedErrors, selectedTab)
-        } else {
-            const diagram = createMermaidDiagram(stateMachine, diagramOrientation);
-            currentDiagram = diagram;
-            root.innerHTML = renderStateMachineView(stateMachine, diagram, selectedTab, diagramOrientation);
-            if (stateMachine) renderMermaidDiagram(document, window);
+        switch (selectedTab) {
+            case 'diagnostics':
+                root.innerHTML = renderDiagnosticsView(diagnostics, showAllDiagnostics, currentFile, expandedErrors);
+                break;
+            case 'fsm':
+                const diagram = createMermaidDiagram(stateMachine, diagramOrientation);
+                currentDiagram = diagram;
+                root.innerHTML = renderStateMachineView(stateMachine, diagram, diagramOrientation);
+                if (stateMachine) renderMermaidDiagram(document, window);
+                break;
+            case 'context':
+                root.innerHTML = renderContextView(context, currentFile, contextSectionState, diagnostics);
+                break;
         }
     }
 }
diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
index f4d5797..2e8a042 100644
--- a/client/src/webview/styles.ts
+++ b/client/src/webview/styles.ts
@@ -264,7 +264,7 @@ export function getStyles(): string {
             margin: 0rem 0;
             background-color: var(--vscode-editor-background);
             border-radius: 4px;
-            overflow: hidden;
+            overflow: visible;
         }
         th {
             text-align: left;
@@ -288,6 +288,90 @@ export function getStyles(): string {
             font-family: var(--vscode-editor-font-family);
             font-size: 0.9em;
         }
+        .context-section {
+            margin-bottom: 1rem;
+        }
+        .context-section table td:first-child {
+            text-align: left;
+            flex: 1;
+            min-width: 0;
+        }
+        .context-section table td:last-child {
+            text-align: right;
+            flex-shrink: 0;
+            white-space: nowrap;
+        }
+        .context-toggle-btn {
+            display: flex;
+            align-items: center;
+            gap: 0.5rem;
+            width: 100%;
+            padding: 0;
+            margin: 0 0 0.5rem 0;
+            background: none;
+            border: none;
+            color: var(--vscode-foreground);
+            cursor: pointer;
+            font-size: 1rem;
+            font-weight: bold;
+            text-align: left;
+        }
+        .context-toggle-btn:hover {
+            background: none;
+        }
+        .context-toggle-icon {
+            width: 1rem;
+            text-align: center;
+            flex-shrink: 0;
+            font-size: larger;
+        }
+        .context-section-content.collapsed {
+            display: none;
+        }
+        .highlight-var-btn {
+            background-color: transparent;
+            border: none;
+            transition: background-color 0.1s;
+            text-align: left;
+        }
+        .highlight-var-btn code {
+            pointer-events: none;
+        }
+        .highlight-var-btn.selected {
+            background-color: var(--vscode-button-background);
+        }
+        .context-variable .failing-refinement {
+            color: var(--vscode-editorError-foreground);
+            font-size: 0.8rem;
+            position: relative;
+        }
+        .context-variable .failing-refinement::after {
+            content: attr(data-tooltip);
+            position: absolute;
+            left: 0;
+            bottom: calc(100% + 0.35rem);
+            min-width: 15rem;
+            max-width: 25rem;
+            padding: 0.5rem 0.65rem;
+            border-radius: 4px;
+            background: var(--vscode-editorHoverWidget-background);
+            border: 1px solid var(--vscode-editorHoverWidget-border);
+            color: var(--vscode-editorHoverWidget-foreground);
+            font-size: 0.8rem;
+            line-height: 1.4;
+            white-space: normal;
+            box-shadow: 0 4px 12px rgba(0, 0, 0, 0.2);
+            opacity: 0;
+            visibility: hidden;
+            pointer-events: none;
+            transition: opacity 0.08s ease, visibility 0.08s ease;
+            transition-delay: 0.08s;
+            z-index: 10;
+        }
+        .context-variable .failing-refinement:hover::after {
+            opacity: 1;
+            visibility: visible;
+        }
         .diagram-section {
             margin-bottom: 1.5rem;
             padding-bottom: 1rem;
diff --git a/client/src/webview/utils.ts b/client/src/webview/utils.ts
new file mode 100644
index 0000000..f20bd89
--- /dev/null
+++ b/client/src/webview/utils.ts
@@ -0,0 +1,18 @@
+
+export function getSimpleName(qualifiedName: string): string {
+    const parts = qualifiedName.split('.');
+    return parts[parts.length - 1];
+}
+
+export function getOriginalVariableName(name: string): string {
+    return name.split("_")[0].replace(/^#/, '');
+}
+
+export function escapeHtml(html: string): string {
+    return html
+        .replace(/&/g, '&amp;')
+        .replace(/"/g, '&quot;')
+        .replace(/'/g, '&#39;')
+        .replace(/</g, '&lt;')
+        .replace(/>/g, '&gt;');
+}
\ No newline at end of file
diff --git a/client/src/webview/views/context/aliases.ts b/client/src/webview/views/context/aliases.ts
new file mode 100644
index 0000000..6cd0f2f
--- /dev/null
+++ b/client/src/webview/views/context/aliases.ts
@@ -0,0 +1,29 @@
+import { LJAlias } from "../../../types/context";
+import { getSimpleName } from "../../utils";
+import { renderToggleSection } from "../sections";
+
+export function renderContextAliases(aliases: LJAlias[], isExpanded: boolean): string {
+    return /*html*/`
+        <div class="context-section">
+            ${renderToggleSection('Aliases', 'context-aliases', isExpanded)}
+            <div id="context-aliases" class="context-section-content ${isExpanded ? '' : 'collapsed'}">
+                ${aliases.length > 0 ? /*html*/`
+                <table>
+                    <tbody>
+                        ${aliases.map(alias => /*html*/`
+                            <tr>
+                                <td>
+                                    <code>
+                                        ${alias.name}(${alias.parameters.map((parameter, index) => `${getSimpleName(alias.types[index])} ${parameter}`).join(", ")}) { ${alias.predicate} }
+                                    </code>
+                                </td>
+                                <td><code>alias</code></td>
+                            </tr>
+                        `).join('')}
+                    </tbody>
+                </table>
+                ` : '<p>No aliases declared in the project</p>'}
+            </div>
+        </div>
+    `;
+}
\ No newline at end of file
diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts
new file mode 100644
index 0000000..218a8be
--- /dev/null
+++ b/client/src/webview/views/context/context.ts
@@ -0,0 +1,32 @@
+import { LJContext } from "../../../types/context";
+import { LJDiagnostic } from "../../../types/diagnostics";
+import { renderMainHeader } from "../sections";
+import { renderContextAliases } from "./aliases";
+import { renderContextGhosts } from "./ghosts";
+import { renderContextVariables } from "./variables";
+
+export type ContextSectionState = {
+    aliases: boolean;
+    ghosts: boolean;
+    vars: boolean;
+}
+
+export function renderContextView(context: LJContext, currentFile: string, sectionState: ContextSectionState, diagnostics: LJDiagnostic[]): string {
+    if (!context || !currentFile) return "";
+
+    const allVars = context.allVars;
+    const ghosts = context.ghosts.filter(ghost => ghost.file === currentFile);
+    const aliases = context.aliases;
+    const total = allVars.length + ghosts.length + aliases.length;
+    return /*html*/`
+        <div>
+            ${renderMainHeader("", 'context')}
+            ${total === 0
+                ? '<p>No context information available at the cursor position</p>'
+                : `${renderContextAliases(aliases, sectionState.aliases)}
+                   ${renderContextGhosts(ghosts, sectionState.ghosts)}
+                   ${renderContextVariables(allVars, sectionState.vars, diagnostics)}
+            `}
+        </div>
+    `;
+}
diff --git a/client/src/webview/views/context/ghosts.ts b/client/src/webview/views/context/ghosts.ts
new file mode 100644
index 0000000..1a50b27
--- /dev/null
+++ b/client/src/webview/views/context/ghosts.ts
@@ -0,0 +1,25 @@
+import { LJGhost } from "../../../types/context";
+import { getSimpleName } from "../../utils";
+import { renderToggleSection } from "../sections";
+
+export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): string {
+    return /*html*/`
+        <div class="context-section">
+            ${renderToggleSection('Ghosts', 'context-ghosts', isExpanded)}
+            <div id="context-ghosts" class="context-section-content ${isExpanded ? '' : 'collapsed'}">
+                ${ghosts.length > 0 ? /*html*/`
+                <table>
+                    <tbody>
+                        ${ghosts.map(ghost => /*html*/`
+                            <tr>
+                                <td><code>${ghost.returnType} ${ghost.name}(${ghost.parameterTypes.map(getSimpleName).join(', ')})</code></td>
+                                <td><code>${ghost.isState ? 'state' : 'ghost'}</code></td>
+                            </tr>
+                        `).join('')}
+                    </tbody>
+                </table>
+                ` : '<p>No ghosts or states declared in the current file</p>'}
+            </div>
+        </div>
+    `;
+}
\ No newline at end of file
diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts
new file mode 100644
index 0000000..2536fa4
--- /dev/null
+++ b/client/src/webview/views/context/variables.ts
@@ -0,0 +1,52 @@
+import { LJVariable } from "../../../types/context";
+import { LJDiagnostic, RefinementError, StateRefinementError } from "../../../types/diagnostics";
+import { escapeHtml, getSimpleName } from "../../utils";
+import { renderToggleSection, renderVariableHighlightButton } from "../sections";
+
+export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, diagnostics: LJDiagnostic[]): string {
+    return /*html*/`
+        <div class="context-section">
+            ${renderToggleSection('Variables', 'context-vars', isExpanded)}
+            <div id="context-vars" class="context-section-content ${isExpanded ? '' : 'collapsed'}">
+                ${variables.length > 0 ? /*html*/`
+                <table>
+                    <tbody>
+                        ${variables.map(variable => /*html*/`
+                            <tr>
+                                <td>${renderVariable(variable, diagnostics)}</td>
+                                <td><code>${getSimpleName(variable.type)}</code></td>
+                            </tr>
+                        `).join('')}
+                    </tbody>
+                </table>
+                `: '<p>No variables declared at the cursor position</p>'}
+            </div>
+        </div>
+    `;
+}
+
+function renderVariable(variable: LJVariable, diagnostics: LJDiagnostic[]): string {
+    const diagnostic = getMatchingDiagnostic(variable, diagnostics);
+    return /*html*/`
+        <div class="context-variable">
+            ${renderVariableHighlightButton(variable.position, variable.refinement)}
+            ${diagnostic ? /*html*/`<code class="failing-refinement" data-tooltip="${escapeHtml(diagnostic.message)}">⊢ ${diagnostic.expected}</code>` : ''}
+        </div>`;
+}
+
+function getMatchingDiagnostic(variable: LJVariable, diagnostics: LJDiagnostic[]): { expected: string, message: string} | null {
+    // find refinement or state refinement error that matches the variable's position
+    const matchingDiagnostic = diagnostics.find(d => {
+        if (!d.position || !variable.position) return false;
+        if (d.type !== 'refinement-error' && d.type !== 'state-refinement-error') return false;
+        return JSON.stringify(d.position) === JSON.stringify(variable.position);
+    }) as RefinementError | StateRefinementError | undefined;
+    if (!matchingDiagnostic) return null;
+
+    // get the expected type from diagnostic
+    const expected = matchingDiagnostic.type == "refinement-error" ? matchingDiagnostic.expected.value : matchingDiagnostic.expected;
+    if (!expected) return null;
+    
+    // only include those that mention the variable 
+    return expected.includes(variable.name) ? { expected, message: `${matchingDiagnostic.title}: ${matchingDiagnostic.message}` } : null;
+}
\ No newline at end of file
diff --git a/client/src/webview/views/verification/derivation-nodes.ts b/client/src/webview/views/diagnostics/derivation-nodes.ts
similarity index 97%
rename from client/src/webview/views/verification/derivation-nodes.ts
rename to client/src/webview/views/diagnostics/derivation-nodes.ts
index 6c90a94..fcd6897 100644
--- a/client/src/webview/views/verification/derivation-nodes.ts
+++ b/client/src/webview/views/diagnostics/derivation-nodes.ts
@@ -35,10 +35,10 @@ function renderJsonTree(
         
         const filePath = (placement as any)?.file ?? error.file;
         const filename = filePath.split("/").pop() ?? "";
-        const tooltipData = `${filename}:${(placement.position?.line ?? 0) + 1}`;
+        const tooltipData = `${filename}:${(placement.position?.lineStart ?? 0) + 1}`;
         const classes = `node-var tooltip clickable ${hasOrigin ? "derivable-node" : ""}`.trim();
         const attrs = hasOrigin ? ` data-node-path="${path}" data-error-id="${errorId}"` : "";
-        const fileAttr = ` data-file="${filePath}" data-line="${placement.position?.line ?? 0}" data-column="${placement.position?.column ?? 0}"`;
+        const fileAttr = ` data-file="${filePath}" data-line="${placement.position?.lineStart ?? 0}" data-column="${placement.position?.colStart ?? 0}"`;
         return `<span class="${classes}" data-tooltip="${tooltipData}"${fileAttr}${attrs}>${node.var}</span>`;
     }
 
diff --git a/client/src/webview/views/verification/verification.ts b/client/src/webview/views/diagnostics/diagnostics.ts
similarity index 91%
rename from client/src/webview/views/verification/verification.ts
rename to client/src/webview/views/diagnostics/diagnostics.ts
index 2e53d4d..2e99663 100644
--- a/client/src/webview/views/verification/verification.ts
+++ b/client/src/webview/views/diagnostics/diagnostics.ts
@@ -1,14 +1,13 @@
 import { LJDiagnostic, LJError, LJWarning } from "../../../types/diagnostics";
 import { renderErrors } from "./errors";
-import { NavTab, renderMainHeader } from "../sections";
+import { renderMainHeader } from "../sections";
 import { renderWarnings } from "./warnings";
 
-export function renderVerificationView(
+export function renderDiagnosticsView(
     diagnostics: LJDiagnostic[],
     showAll: boolean,
     currentFile: string,
     expandedErrors: Set<number>,
-    selectedTab: NavTab
 ): string {
     const fileDiagnostics = diagnostics.filter(diagnostic => diagnostic.file?.toLowerCase() === currentFile?.toLowerCase() || !diagnostic.file);
     const displayDiagnostics = showAll ? diagnostics : fileDiagnostics;
@@ -24,7 +23,7 @@ export function renderVerificationView(
     
     return /*html*/`
         <div>
-            ${renderMainHeader(titleMessage, selectedTab)}
+            ${renderMainHeader(titleMessage, 'diagnostics')}
             <p class="info">${infoMessage}</p>
             ${
                 diagnostics.length === 0 ? '' : /*html*/`
diff --git a/client/src/webview/views/verification/errors.ts b/client/src/webview/views/diagnostics/errors.ts
similarity index 94%
rename from client/src/webview/views/verification/errors.ts
rename to client/src/webview/views/diagnostics/errors.ts
index 3fcf35f..da3f944 100644
--- a/client/src/webview/views/verification/errors.ts
+++ b/client/src/webview/views/diagnostics/errors.ts
@@ -1,4 +1,4 @@
-import { renderHeader, renderLocation, renderSection, renderCustomSection, renderTranslationTable,  } from "../sections";
+import { renderDiagnosticHeader, renderLocation, renderSection, renderCustomSection, renderTranslationTable,  } from "../sections";
 import { renderDerivationNode } from "./derivation-nodes";
 import type {
     ArgumentMismatchError,
@@ -58,7 +58,7 @@ const errorContentRenderers: Partial<Record<LJError['type'], (error: LJError) =>
 };
 
 export function renderError(error: LJError, errorIndex: number, isExpanded: boolean): string {
-    const header = renderHeader(error);
+    const header = renderDiagnosticHeader(error);
     const content = errorContentRenderers[error.type]?.(error) ?? '';
     const location = renderLocation(error);
     const extra = renderExtra(error, errorIndex, isExpanded);
diff --git a/client/src/webview/views/verification/warnings.ts b/client/src/webview/views/diagnostics/warnings.ts
similarity index 89%
rename from client/src/webview/views/verification/warnings.ts
rename to client/src/webview/views/diagnostics/warnings.ts
index 8660467..dde140e 100644
--- a/client/src/webview/views/verification/warnings.ts
+++ b/client/src/webview/views/diagnostics/warnings.ts
@@ -1,5 +1,5 @@
 import type { ExternalClassNotFoundWarning, ExternalMethodNotFoundWarning, LJWarning } from "../../../types/diagnostics";
-import { renderHeader, renderLocation, renderSection } from "../sections";
+import { renderDiagnosticHeader, renderLocation, renderSection } from "../sections";
 
 export function renderWarnings(warnings: LJWarning[]): string {
     return /*html*/`
@@ -24,7 +24,7 @@ const warningContentRenderers: Partial<Record<LJWarning['type'], (warning: LJWar
 };
 
 export function renderWarning(warning: LJWarning): string {
-    const header = renderHeader(warning);
+    const header = renderDiagnosticHeader(warning);
     const content = warningContentRenderers[warning.type]?.(warning) ?? '';
     const location = renderLocation(warning);
     return /*html*/`${header}${content}${location}`;
diff --git a/client/src/webview/views/diagram.ts b/client/src/webview/views/fsm/fsm.ts
similarity index 83%
rename from client/src/webview/views/diagram.ts
rename to client/src/webview/views/fsm/fsm.ts
index a0374cf..593a162 100644
--- a/client/src/webview/views/diagram.ts
+++ b/client/src/webview/views/fsm/fsm.ts
@@ -1,13 +1,12 @@
-import type { StateMachine } from "../../types/fsm";
-import { renderMainHeader, type NavTab } from "./sections";
+import type { LJStateMachine } from "../../../types/fsm";
+import { renderMainHeader } from "../sections";
 
-export function renderStateMachineView(sm: StateMachine, diagram: string, selectedTab: NavTab = 'state-machine', orientation: "LR" | "TB"): string {
+export function renderStateMachineView(sm: LJStateMachine, diagram: string, orientation: "LR" | "TB"): string {
     return /*html*/`
         <div>
-            ${renderMainHeader("", selectedTab)}
+            ${renderMainHeader("", 'fsm')}
             ${sm ? /*html*/`
                 <div class="diagram-section">
-                    
                     <div class="diagram-container">
                         <div class="diagram-controls">
                             <button id="zoom-in-btn" class="diagram-control-btn" title="Zoom In">+</button>
diff --git a/client/src/webview/views/loading.ts b/client/src/webview/views/loading.ts
index 9225421..4549f0e 100644
--- a/client/src/webview/views/loading.ts
+++ b/client/src/webview/views/loading.ts
@@ -3,7 +3,7 @@ export function renderLoading(): string {
     return /*html*/`
         <div>
             <h2>LiquidJava</h2>
-            <p>Starting verification...</p>
+            <p>Loading extension...</p>
         </div>
     `;
 }
diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts
index 5e184c1..6705edb 100644
--- a/client/src/webview/views/sections.ts
+++ b/client/src/webview/views/sections.ts
@@ -1,4 +1,4 @@
-import type { LJDiagnostic, TranslationTable } from "../../types/diagnostics";
+import type { LJDiagnostic, PlacementInCode, SourcePosition, TranslationTable } from "../../types/diagnostics";
 
 export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
     <div class="header">
@@ -13,16 +13,19 @@ export const renderCustomSection = (title: string, body: string): string => /*ht
 export const renderSection = (title: string, body: string): string => /*html*/
     renderCustomSection(title, `<pre>${body}</pre>`);
 
-export const renderHeader = (diagnostic: LJDiagnostic): string => /*html*/
+export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/`
+    <button class="context-toggle-btn" data-context-toggle="${targetId}" aria-expanded="${isExpanded ? 'true' : 'false'}" type="button">
+        <span class="context-toggle-icon">${isExpanded ? '▾' : '▸'}</span>
+        <span>${title}</span>
+    </button>
+    `;
+
+export const renderDiagnosticHeader = (diagnostic: LJDiagnostic): string => /*html*/
     `<h3>${diagnostic.title}</h3><div class="diagnostic-header"><p>${diagnostic.message}</p></div>`;
 
 export const renderLocation = (diagnostic: LJDiagnostic): string => {
-    if (!diagnostic.position) return "";
-    const line = diagnostic.position?.lineStart ?? 0;
-    const column = diagnostic.position?.colStart ?? 0;
-    const simpleFile = diagnostic.file.split('/').pop() || diagnostic.file;
-    const link = /*html*/`<a href="#" class="link location-link" data-file="${diagnostic.file}" data-line="${line}" data-column="${column}">${simpleFile}:${line}</a>`;
-    return renderCustomSection("Location", /*html*/`<pre>${link}</pre>`);
+    if (!diagnostic.position || !diagnostic.file) return "";
+    return renderCustomSection("Location", /*html*/`<pre>${renderLocationLink(diagnostic.position)}</pre>`);
 };
 
 export function renderTranslationTable(translationTable: TranslationTable): string {  
@@ -37,27 +40,14 @@ export function renderTranslationTable(translationTable: TranslationTable): stri
                     <tr>
                         <th>Variable</th>
                         <th>Source</th>
-                        <th>Location</th>
                     </tr>
                 </thead>
                 <tbody>
-                    ${entries.map(([variable, placement]: [string, any]) => {
-                        const simpleFile = placement.position.file.split('/').pop() || placement.position.file;
-                        const link = 
-                            /*html*/`<a
-                                href="#"
-                                class="link location-link"
-                                data-file="${placement.position.file}"
-                                data-line="${placement.position.line}"
-                                data-column="${placement.position.column}"
-                            >
-                                ${simpleFile}:${placement.position.line}
-                            </a>`;
+                    ${entries.map(([variable, placement]: [string, PlacementInCode]) => {
                         return /*html*/`
                             <tr>
                                 <td><code>${variable}</code></td>
-                                <td><code>${placement.text}</code></td>
-                                <td>${link}</td>
+                                <td>${renderVariableHighlightButton(placement.position, placement.text)}</td>
                             </tr>
                         `;
                     }).join('')}
@@ -67,15 +57,46 @@ export function renderTranslationTable(translationTable: TranslationTable): stri
     `;
 }
 
-export type NavTab = 'verification' | 'state-machine';
+export function renderVariableHighlightButton(position: SourcePosition, content: string): string {
+    return /*html*/`
+        <button
+            class="highlight-var-btn"
+            data-start-line="${position.lineStart}"
+            data-start-column="${position.colStart}"
+            data-end-line="${position.lineEnd}"
+            data-end-column="${position.colEnd}"
+            data-file="${position.file}"
+        >
+            <code>${content}</code>
+        </button>
+    `;
+}
+
+export function renderLocationLink(position?: SourcePosition): string {
+    if (!position) return 'No location';
+    return /*html*/`<a
+        href="#"
+        class="link location-link"
+        data-file="${position.file}"
+        data-line="${position.lineStart}"
+        data-column="${position.colStart}"
+    >${getFile(position)}</a>`;
+}
+
+function getFile(position: SourcePosition): string {
+    return `${position.file.split('/').pop().trim() || position.file}:${position.lineStart + 1}`;
+}
+
+export type NavTab = 'diagnostics' | 'fsm' | 'context';
 
 export function renderNav(selectedTab: NavTab): string {
     return /*html*/`
         <nav>
             <ul>
-                <li><button class="nav-tab ${selectedTab === 'verification' ? 'selected' : ''}" data-tab="verification">Verification</button></li>
-                <li><button class="nav-tab ${selectedTab === 'state-machine' ? 'selected' : ''}" data-tab="state-machine">State Machine</button></li>
+                <li><button class="nav-tab ${selectedTab === 'diagnostics' ? 'selected' : ''}" data-tab="diagnostics">Verification</button></li>
+                <li><button class="nav-tab ${selectedTab === 'context' ? 'selected' : ''}" data-tab="context">Context</button></li>
+                <li><button class="nav-tab ${selectedTab === 'fsm' ? 'selected' : ''}" data-tab="fsm">State Machine</button></li>
             </ul>
         </nav>
     `;
-}
\ No newline at end of file
+}
diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java
index ca6902c..92024a6 100644
--- a/server/src/main/java/LJDiagnosticsHandler.java
+++ b/server/src/main/java/LJDiagnosticsHandler.java
@@ -10,13 +10,14 @@
 import org.eclipse.lsp4j.Position;
 import org.eclipse.lsp4j.PublishDiagnosticsParams;
 import org.eclipse.lsp4j.Range;
+
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.Diagnostics;
-import liquidjava.diagnostics.ErrorPosition;
 import liquidjava.diagnostics.LJDiagnostic;
 import liquidjava.diagnostics.errors.CustomError;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.warnings.LJWarning;
+import spoon.reflect.cu.SourcePosition;
 import utils.PathUtils;
 
 public class LJDiagnosticsHandler {
@@ -76,7 +77,7 @@ public static List<PublishDiagnosticsParams> getDiagnostics(List<LJDiagnostic> d
             .collect(Collectors.groupingBy(
                 d -> PathUtils.toFileUri(d.getFile()),
                 Collectors.mapping(d -> {
-                    Range range = getRangeFromErrorPosition(d.getPosition());
+                    Range range = getRangeFromPosition(d.getPosition());
                     String message = String.format("%s: %s", d.getTitle(), d.getMessage());
                     return new Diagnostic(range, message, severity, SOURCE);
                 }, Collectors.toList())
@@ -98,16 +99,18 @@ public static PublishDiagnosticsParams getEmptyDiagnostics(String uri) {
     }
 
     /**
-     * Gets the Range from the given ErrorPosition If the position is null, returns a default Range at (0,0)-(0,0)
-     * @param pos the ErrorPosition
+     * Gets the Range from the given SourcePosition If the position is null, returns a default Range at (0,0)-(0,0)
+     * @param pos the SourcePosition
      * @return Range
      */
-    private static Range getRangeFromErrorPosition(ErrorPosition pos) {
+    public static Range getRangeFromPosition(SourcePosition pos) {
         if (pos == null) {
             // no location information available
             return new Range(new Position(0, 0), new Position(0, 0));
         }
-        return new Range(new Position(pos.lineStart() - 1, pos.colStart() - 1),
-                new Position(pos.lineEnd() - 1, pos.colEnd() - 1));
+        return new Range(
+            new Position(pos.getLine() - 1, pos.getColumn() - 1),
+            new Position(pos.getEndLine() - 1, pos.getEndColumn() - 1)
+        );
     }
 }
diff --git a/server/src/main/java/dtos/context/ContextHistoryDTO.java b/server/src/main/java/dtos/context/ContextHistoryDTO.java
index 2f3f86d..32c656b 100644
--- a/server/src/main/java/dtos/context/ContextHistoryDTO.java
+++ b/server/src/main/java/dtos/context/ContextHistoryDTO.java
@@ -3,17 +3,18 @@
 import java.util.List;
 import java.util.Map;
 
+import dtos.diagnostics.SourcePositionDTO;
 import spoon.reflect.reference.CtTypeReference;
 
 /**
  * DTO for serializing ContextHistory instances to JSON.
  */
 public record ContextHistoryDTO(
-    Map<String, Map<String, List<VariableDTO>>> vars,
-    List<VariableDTO> instanceVars,
+    List<VariableDTO> localVars,
     List<VariableDTO> globalVars,
-    Map<String, List<GhostDTO>> ghosts,
-    List<AliasDTO> aliases
+    List<GhostDTO> ghosts,
+    List<AliasDTO> aliases,
+    Map<String, List<SourcePositionDTO>> fileScopes
 ) {
     public static String stringifyType(CtTypeReference<?> typeReference) {
         if (typeReference == null)
diff --git a/server/src/main/java/dtos/context/GhostDTO.java b/server/src/main/java/dtos/context/GhostDTO.java
index 968852b..825d796 100644
--- a/server/src/main/java/dtos/context/GhostDTO.java
+++ b/server/src/main/java/dtos/context/GhostDTO.java
@@ -1,6 +1,7 @@
 package dtos.context;
 
 import java.util.List;
+import java.util.regex.Pattern;
 import java.util.stream.Collectors;
 
 import liquidjava.processor.context.GhostState;
@@ -13,15 +14,24 @@ public record GhostDTO(
     String qualifiedName,
     String returnType,
     List<String> parameterTypes,
-    String refinement
+    String refinement,
+    boolean isState,
+    String file
 ) {
+    private static final Pattern STATE_REFINEMENT_PATTERN = Pattern.compile("^state\\d+\\(_\\) == \\d+$");
+
     public static GhostDTO from(GhostState ghostState) {
+        String refinement = ghostState.getRefinement() != null ? ghostState.getRefinement().toString() : null;
+        boolean isState = refinement != null && STATE_REFINEMENT_PATTERN.matcher(refinement).matches();
+
         return new GhostDTO(
             ghostState.getName(),
             ghostState.getQualifiedName(),
             ContextHistoryDTO.stringifyType(ghostState.getReturnType()),
             ghostState.getParametersTypes().stream().map(ContextHistoryDTO::stringifyType).collect(Collectors.toList()),
-            ghostState.getRefinement() != null ? ghostState.getRefinement().toString() : null
+            refinement,
+            isState,
+            ghostState.getFile()
         );
     }
 }
\ No newline at end of file
diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java
index f89148e..60cada2 100644
--- a/server/src/main/java/dtos/context/VariableDTO.java
+++ b/server/src/main/java/dtos/context/VariableDTO.java
@@ -1,7 +1,7 @@
 package dtos.context;
 
-import dtos.diagnostics.PlacementInCodeDTO;
 import dtos.diagnostics.SourcePositionDTO;
+import liquidjava.processor.context.PlacementInCode;
 import liquidjava.processor.context.RefinedVariable;
 
 /**
@@ -12,19 +12,19 @@ public record VariableDTO(
     String type,
     String refinement,
     String mainRefinement,
-    PlacementInCodeDTO placementInCode,
-    boolean isParameter,
-    SourcePositionDTO annPosition
+    SourcePositionDTO position,
+    SourcePositionDTO annotationPosition
 ) {
     public static VariableDTO from(RefinedVariable refinedVariable) {
+        PlacementInCode placement = refinedVariable.getPlacementInCode();
+        if (placement == null) return null;
         return new VariableDTO(
             refinedVariable.getName(),
             ContextHistoryDTO.stringifyType(refinedVariable.getType()),
             refinedVariable.getRefinement().toString(),
             refinedVariable.getMainRefinement().toString(),
-            PlacementInCodeDTO.from(refinedVariable.getPlacementInCode()),
-            refinedVariable.isParameter(),
-            SourcePositionDTO.from(refinedVariable.getAnnPosition())
+            SourcePositionDTO.from(placement.getPosition()),
+            SourcePositionDTO.from(placement.getAnnotationPosition())
         );
     }
 }
\ No newline at end of file
diff --git a/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java b/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java
index eb15967..7ae1de3 100644
--- a/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java
+++ b/server/src/main/java/dtos/diagnostics/LJDiagnosticDTO.java
@@ -1,15 +1,14 @@
 package dtos.diagnostics;
 
 import liquidjava.diagnostics.LJDiagnostic;
-import liquidjava.diagnostics.ErrorPosition;
 
 /**
  * DTO for serializing LJDiagnostic instances to JSON
  */
-public record LJDiagnosticDTO(String title, String message, String details, String file, ErrorPosition position) {
+public record LJDiagnosticDTO(String title, String message, String details, String file, SourcePositionDTO position) {
 
     public static LJDiagnosticDTO from(LJDiagnostic diagnostic) {
         return new LJDiagnosticDTO(diagnostic.getTitle(), diagnostic.getMessage(), diagnostic.getDetails(),
-                diagnostic.getFile(), diagnostic.getPosition());
+                diagnostic.getFile(), SourcePositionDTO.from(diagnostic.getPosition()));
     }
 }
diff --git a/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java b/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java
index 1e6f6f3..d00595e 100644
--- a/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java
+++ b/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java
@@ -1,14 +1,28 @@
 package dtos.diagnostics;
 
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
 import spoon.reflect.cu.SourcePosition;
 
-/**
- * DTO for serializing Spoon SourcePosition to JSON
- */
-public record SourcePositionDTO(String file, int line, int column) {
+public record SourcePositionDTO(String file, int lineStart, int colStart, int lineEnd, int colEnd) {
+
+    public static SourcePositionDTO from(SourcePosition pos) {
+        if (pos == null) return null;
+        String file = pos.getFile() != null ? pos.getFile().getAbsolutePath() : null;
+        return new SourcePositionDTO(file, pos.getLine() - 1, pos.getColumn() - 1, pos.getEndLine() - 1, pos.getEndColumn());
+    }
+
+    public static SourcePositionDTO from(String pos) {
+        if (pos == null) return null;
+        Pattern p = Pattern.compile("(\\d+):(\\d+)-(\\d+):(\\d+)");
+        Matcher m = p.matcher(pos);
+        if (!m.matches()) return null;
 
-    public static SourcePositionDTO from(SourcePosition position) {
-        String file = position.getFile() != null ? position.getFile().getAbsolutePath() : "";
-        return new SourcePositionDTO(file, position.getLine() - 1, position.getColumn() - 1);
+        int line = Integer.parseInt(m.group(1));
+        int column = Integer.parseInt(m.group(2));
+        int endLine = Integer.parseInt(m.group(3));
+        int endColumn = Integer.parseInt(m.group(4));
+        return new SourcePositionDTO(null, line - 1, column - 1, endLine - 1, endColumn);
     }
 }
diff --git a/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java b/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java
index facff9f..710520c 100644
--- a/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java
+++ b/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java
@@ -1,16 +1,16 @@
 package dtos.errors;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.errors.ArgumentMismatchError;
 
 /**
  * DTO for serializing ArgumentMismatchErrorDTO instances to JSON
  */
 public record ArgumentMismatchErrorDTO(String category, String type, String title, String message, String file,
-        ErrorPosition position) {
+        SourcePositionDTO position) {
 
     public static ArgumentMismatchErrorDTO from(ArgumentMismatchError error) {
         return new ArgumentMismatchErrorDTO("error", "argument-mismatch-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition());
+                SourcePositionDTO.from(error.getPosition()));
     }
 }
diff --git a/server/src/main/java/dtos/errors/CustomErrorDTO.java b/server/src/main/java/dtos/errors/CustomErrorDTO.java
index c097eb4..38b4e04 100644
--- a/server/src/main/java/dtos/errors/CustomErrorDTO.java
+++ b/server/src/main/java/dtos/errors/CustomErrorDTO.java
@@ -1,15 +1,15 @@
 package dtos.errors;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.errors.CustomError;
 
 /**
  * DTO for serializing CustomError instances to JSON
  */
-public record CustomErrorDTO(String category, String type, String title, String message, String file, ErrorPosition position) {
+public record CustomErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position) {
 
     public static CustomErrorDTO from(CustomError error) {
         return new CustomErrorDTO("error", "custom-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition());
+                SourcePositionDTO.from(error.getPosition()));
     }
 }
diff --git a/server/src/main/java/dtos/errors/IllegalConstructorTransitionErrorDTO.java b/server/src/main/java/dtos/errors/IllegalConstructorTransitionErrorDTO.java
index 5953743..d2695f6 100644
--- a/server/src/main/java/dtos/errors/IllegalConstructorTransitionErrorDTO.java
+++ b/server/src/main/java/dtos/errors/IllegalConstructorTransitionErrorDTO.java
@@ -1,16 +1,16 @@
 package dtos.errors;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.errors.IllegalConstructorTransitionError;
 
 /**
  * DTO for serializing IllegalConstructorTransitionError instances to JSON
  */
 public record IllegalConstructorTransitionErrorDTO(String category, String type, String title, String message, String file,
-        ErrorPosition position) {
+        SourcePositionDTO position) {
 
     public static IllegalConstructorTransitionErrorDTO from(IllegalConstructorTransitionError error) {
         return new IllegalConstructorTransitionErrorDTO("error", "illegal-constructor-transition-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition());
+                SourcePositionDTO.from(error.getPosition()));
     }
 }
diff --git a/server/src/main/java/dtos/errors/InvalidRefinementErrorDTO.java b/server/src/main/java/dtos/errors/InvalidRefinementErrorDTO.java
index b189ff2..a669da4 100644
--- a/server/src/main/java/dtos/errors/InvalidRefinementErrorDTO.java
+++ b/server/src/main/java/dtos/errors/InvalidRefinementErrorDTO.java
@@ -1,16 +1,16 @@
 package dtos.errors;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.errors.InvalidRefinementError;
 
 /**
  * DTO for serializing InvalidRefinementError instances to JSON
  */
 public record InvalidRefinementErrorDTO(String category, String type, String title, String message, String file,
-        ErrorPosition position, String refinement) {
+        SourcePositionDTO position, String refinement) {
 
     public static InvalidRefinementErrorDTO from(InvalidRefinementError error) {
         return new InvalidRefinementErrorDTO("error", "invalid-refinement-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition(), error.getRefinement());
+                SourcePositionDTO.from(error.getPosition()), error.getRefinement());
     }
 }
diff --git a/server/src/main/java/dtos/errors/LJErrorDTO.java b/server/src/main/java/dtos/errors/LJErrorDTO.java
index edab2e8..67c0865 100644
--- a/server/src/main/java/dtos/errors/LJErrorDTO.java
+++ b/server/src/main/java/dtos/errors/LJErrorDTO.java
@@ -1,17 +1,17 @@
 package dtos.errors;
 
+import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.TranslationTableDTO;
-import liquidjava.diagnostics.ErrorPosition;
 import liquidjava.diagnostics.errors.LJError;
 
 /**
  * DTO for serializing LJError instances to JSON
  */
-public record LJErrorDTO(String title, String message, String file, ErrorPosition position,
+public record LJErrorDTO(String title, String message, String file, SourcePositionDTO position,
         TranslationTableDTO translationTable) {
 
     public static LJErrorDTO from(LJError error) {
         return new LJErrorDTO(error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition(), TranslationTableDTO.from(error.getTranslationTable()));
+                SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()));
     }
 }
diff --git a/server/src/main/java/dtos/errors/NotFoundErrorDTO.java b/server/src/main/java/dtos/errors/NotFoundErrorDTO.java
index 79b7c97..bc8ae7a 100644
--- a/server/src/main/java/dtos/errors/NotFoundErrorDTO.java
+++ b/server/src/main/java/dtos/errors/NotFoundErrorDTO.java
@@ -1,17 +1,17 @@
 package dtos.errors;
 
+import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.TranslationTableDTO;
-import liquidjava.diagnostics.ErrorPosition;
 import liquidjava.diagnostics.errors.NotFoundError;
 
 /**
  * DTO for serializing NotFoundError instances to JSON
  */
-public record NotFoundErrorDTO(String category, String type, String title, String message, String file, ErrorPosition position,
+public record NotFoundErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position,
         TranslationTableDTO translationTable, String name, String kind) {
 
     public static NotFoundErrorDTO from(NotFoundError error) {
         return new NotFoundErrorDTO("error", "not-found-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition(), TranslationTableDTO.from(error.getTranslationTable()), error.getName(), error.getKind());
+                SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()), error.getName(), error.getKind());
     }
 }
diff --git a/server/src/main/java/dtos/errors/RefinementErrorDTO.java b/server/src/main/java/dtos/errors/RefinementErrorDTO.java
index bea838b..18f1d7a 100644
--- a/server/src/main/java/dtos/errors/RefinementErrorDTO.java
+++ b/server/src/main/java/dtos/errors/RefinementErrorDTO.java
@@ -1,18 +1,18 @@
 package dtos.errors;
 
+import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.TranslationTableDTO;
-import liquidjava.diagnostics.ErrorPosition;
 import liquidjava.diagnostics.errors.RefinementError;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 
 /**
  * DTO for serializing RefinementError instances to JSON
  */
-public record RefinementErrorDTO(String category, String type, String title, String message, String file, ErrorPosition position,
+public record RefinementErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position,
         TranslationTableDTO translationTable, ValDerivationNode expected, ValDerivationNode found, String customMessage, String counterexample) {
 
     public static RefinementErrorDTO from(RefinementError error) {
         return new RefinementErrorDTO("error", "refinement-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition(), TranslationTableDTO.from(error.getTranslationTable()), error.getExpected(), error.getFound(), error.getCustomMessage(), error.getCounterExampleString());
+                SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()), error.getExpected(), error.getFound(), error.getCustomMessage(), error.getCounterExampleString());
     }
 }
diff --git a/server/src/main/java/dtos/errors/StateConflictErrorDTO.java b/server/src/main/java/dtos/errors/StateConflictErrorDTO.java
index 3c84a37..402e1bd 100644
--- a/server/src/main/java/dtos/errors/StateConflictErrorDTO.java
+++ b/server/src/main/java/dtos/errors/StateConflictErrorDTO.java
@@ -1,17 +1,17 @@
 package dtos.errors;
 
+import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.TranslationTableDTO;
-import liquidjava.diagnostics.ErrorPosition;
 import liquidjava.diagnostics.errors.StateConflictError;
 
 /**
  * DTO for serializing StateConflictError instances to JSON
  */
-public record StateConflictErrorDTO(String category, String type, String title, String message, String file, ErrorPosition position,
+public record StateConflictErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position,
         TranslationTableDTO translationTable, String state) {
 
     public static StateConflictErrorDTO from(StateConflictError error) {
         return new StateConflictErrorDTO("error", "state-conflict-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition(), TranslationTableDTO.from(error.getTranslationTable()), error.getState());
+                SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()), error.getState());
     }
 }
diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java
index 3a032c8..5bcd7c7 100644
--- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java
+++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java
@@ -1,18 +1,18 @@
 package dtos.errors;
 
+import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.TranslationTableDTO;
-import liquidjava.diagnostics.ErrorPosition;
 import liquidjava.diagnostics.errors.StateRefinementError;
 
 /**
  * DTO for serializing StateRefinementError instances to JSON
  */
-public record StateRefinementErrorDTO(String category, String type, String title, String message, String file, ErrorPosition position,
+public record StateRefinementErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position,
         TranslationTableDTO translationTable, String expected, String found, String customMessage) {
 
     public static StateRefinementErrorDTO from(StateRefinementError error) {
         return new StateRefinementErrorDTO("error", "state-refinement-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition(), TranslationTableDTO.from(error.getTranslationTable()), error.getExpected(),
+                SourcePositionDTO.from(error.getPosition()), TranslationTableDTO.from(error.getTranslationTable()), error.getExpected(),
                 error.getFound(), error.getCustomMessage());
     }
 }
diff --git a/server/src/main/java/dtos/errors/SyntaxErrorDTO.java b/server/src/main/java/dtos/errors/SyntaxErrorDTO.java
index 00b0a01..e426823 100644
--- a/server/src/main/java/dtos/errors/SyntaxErrorDTO.java
+++ b/server/src/main/java/dtos/errors/SyntaxErrorDTO.java
@@ -1,16 +1,16 @@
 package dtos.errors;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.errors.SyntaxError;
 
 /**
  * DTO for serializing SyntaxError instances to JSON
  */
-public record SyntaxErrorDTO(String category, String type, String title, String message, String file, ErrorPosition position,
+public record SyntaxErrorDTO(String category, String type, String title, String message, String file, SourcePositionDTO position,
         String refinement) {
 
     public static SyntaxErrorDTO from(SyntaxError error) {
         return new SyntaxErrorDTO("error", "syntax-error", error.getTitle(), error.getMessage(), error.getFile(),
-                error.getPosition(), error.getRefinement());
+                SourcePositionDTO.from(error.getPosition()), error.getRefinement());
     }
 }
diff --git a/server/src/main/java/dtos/warnings/CustomWarningDTO.java b/server/src/main/java/dtos/warnings/CustomWarningDTO.java
index ccfebfc..5e02122 100644
--- a/server/src/main/java/dtos/warnings/CustomWarningDTO.java
+++ b/server/src/main/java/dtos/warnings/CustomWarningDTO.java
@@ -1,15 +1,15 @@
 package dtos.warnings;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.warnings.CustomWarning;
 
 /**
  * DTO for serializing CustomError instances to JSON
  */
-public record CustomWarningDTO(String category, String type, String title, String message, String file, ErrorPosition position) {
+public record CustomWarningDTO(String category, String type, String title, String message, String file, SourcePositionDTO position) {
 
     public static CustomWarningDTO from(CustomWarning warning) {
         return new CustomWarningDTO("warning", "custom-warning", warning.getTitle(), warning.getMessage(), warning.getFile(),
-                warning.getPosition());
+                SourcePositionDTO.from(warning.getPosition()));
     }
 }
diff --git a/server/src/main/java/dtos/warnings/ExternalClassNotFoundWarningDTO.java b/server/src/main/java/dtos/warnings/ExternalClassNotFoundWarningDTO.java
index b073b0a..36a0d86 100644
--- a/server/src/main/java/dtos/warnings/ExternalClassNotFoundWarningDTO.java
+++ b/server/src/main/java/dtos/warnings/ExternalClassNotFoundWarningDTO.java
@@ -1,16 +1,16 @@
 package dtos.warnings;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning;
 
 /**
  * DTO for serializing ExternalClassNotFoundWarning instances to JSON
  */
 public record ExternalClassNotFoundWarningDTO(String category, String type, String title, String message, String file,
-        ErrorPosition position, String className) {
+        SourcePositionDTO position, String className) {
 
     public static ExternalClassNotFoundWarningDTO from(ExternalClassNotFoundWarning warning) {
         return new ExternalClassNotFoundWarningDTO("warning", "external-class-not-found-warning", warning.getTitle(), warning.getMessage(), warning.getFile(),
-                warning.getPosition(), warning.getClassName());
+                SourcePositionDTO.from(warning.getPosition()), warning.getClassName());
     }
 }
diff --git a/server/src/main/java/dtos/warnings/ExternalMethodNotFoundWarningDTO.java b/server/src/main/java/dtos/warnings/ExternalMethodNotFoundWarningDTO.java
index 2c9a2d9..71752a8 100644
--- a/server/src/main/java/dtos/warnings/ExternalMethodNotFoundWarningDTO.java
+++ b/server/src/main/java/dtos/warnings/ExternalMethodNotFoundWarningDTO.java
@@ -1,16 +1,16 @@
 package dtos.warnings;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning;
 
 /**
  * DTO for serializing ExternalMethodNotFoundWarning instances to JSON
  */
 public record ExternalMethodNotFoundWarningDTO(String category, String type, String title, String message, String file,
-        ErrorPosition position, String methodName, String className, String[] overloads) {
+        SourcePositionDTO position, String methodName, String className, String[] overloads) {
 
     public static ExternalMethodNotFoundWarningDTO from(ExternalMethodNotFoundWarning warning) {
         return new ExternalMethodNotFoundWarningDTO("warning", "external-method-not-found-warning", warning.getTitle(), warning.getMessage(), warning.getFile(),
-                warning.getPosition(), warning.getMethodName(), warning.getClassName(), warning.getOverloads());
+                SourcePositionDTO.from(warning.getPosition()), warning.getMethodName(), warning.getClassName(), warning.getOverloads());
     }
 }
diff --git a/server/src/main/java/dtos/warnings/LJWarningDTO.java b/server/src/main/java/dtos/warnings/LJWarningDTO.java
index 4c7a0a6..acd598a 100644
--- a/server/src/main/java/dtos/warnings/LJWarningDTO.java
+++ b/server/src/main/java/dtos/warnings/LJWarningDTO.java
@@ -1,14 +1,14 @@
 package dtos.warnings;
 
-import liquidjava.diagnostics.ErrorPosition;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.diagnostics.warnings.LJWarning;
 
 /**
  * DTO for serializing LJWarning instances to JSON
  */
-public record LJWarningDTO(String title, String message, String file, ErrorPosition position) {
+public record LJWarningDTO(String title, String message, String file, SourcePositionDTO position) {
 
     public static LJWarningDTO from(LJWarning warning) {
-        return new LJWarningDTO(warning.getTitle(), warning.getMessage(), warning.getFile(), warning.getPosition());
+        return new LJWarningDTO(warning.getTitle(), warning.getMessage(), warning.getFile(), SourcePositionDTO.from(warning.getPosition()));
     }
 }
diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java
index cfc19e2..10858fd 100644
--- a/server/src/main/java/utils/ContextHistoryConverter.java
+++ b/server/src/main/java/utils/ContextHistoryConverter.java
@@ -10,9 +10,8 @@
 import dtos.context.ContextHistoryDTO;
 import dtos.context.GhostDTO;
 import dtos.context.VariableDTO;
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.processor.context.ContextHistory;
-import liquidjava.processor.context.GhostState;
-import liquidjava.processor.context.RefinedVariable;
 
 /**
  * Utility class for converting LiquidJava context objects to DTOs.
@@ -26,32 +25,18 @@ public class ContextHistoryConverter {
      */
     public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) {
         return new ContextHistoryDTO(
-            toVariablesMap(contextHistory.getFileScopeVars()),
-            contextHistory.getInstanceVars().stream().map(VariableDTO::from).collect(Collectors.toList()),
-            contextHistory.getGlobalVars().stream().map(VariableDTO::from).collect(Collectors.toList()),
-            toGhostsMap(contextHistory.getGhosts()),
-            contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList())
+            contextHistory.getLocalVars().stream().map(VariableDTO::from).filter(v -> v != null).collect(Collectors.toList()),
+            contextHistory.getGlobalVars().stream().map(VariableDTO::from).filter(v -> v != null).collect(Collectors.toList()),
+            contextHistory.getGhosts().stream().map(GhostDTO::from).collect(Collectors.toList()),
+            contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()),
+            parseFileScopes(contextHistory.getFileScopes())
         );
     }
 
-    private static Map<String, Map<String, List<VariableDTO>>> toVariablesMap(Map<String, Map<String, Set<RefinedVariable>>> vars) {
-        return vars.entrySet().stream().collect(Collectors.toMap(
+    private static Map<String, List<SourcePositionDTO>> parseFileScopes(Map<String, Set<String>> fileScopes) {
+        return fileScopes.entrySet().stream().collect(Collectors.toMap(
             Map.Entry::getKey,
-            entry -> entry.getValue().entrySet().stream().collect(Collectors.toMap(
-                Map.Entry::getKey,
-                innerEntry -> innerEntry.getValue().stream().map(VariableDTO::from).collect(Collectors.toList()),
-                (left, right) -> left,
-                HashMap::new
-            )),
-            (left, right) -> left,
-            HashMap::new
-        ));
-    }
-
-    private static Map<String, List<GhostDTO>> toGhostsMap(Map<String, Set<GhostState>> ghosts) {
-        return ghosts.entrySet().stream().collect(Collectors.toMap(
-            Map.Entry::getKey,
-            entry -> entry.getValue().stream().map(GhostDTO::from).collect(Collectors.toList()),
+            entry -> entry.getValue().stream().map(SourcePositionDTO::from).collect(Collectors.toList()),
             (left, right) -> left,
             HashMap::new
         ));
diff --git a/server/src/test/java/fsm/StateMachineParserTests.java b/server/src/test/java/fsm/StateMachineParserTests.java
index 27a4266..daad9c4 100644
--- a/server/src/test/java/fsm/StateMachineParserTests.java
+++ b/server/src/test/java/fsm/StateMachineParserTests.java
@@ -2,7 +2,6 @@
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
 
-import java.lang.Thread.State;
 import java.util.List;
 
 import org.junit.jupiter.api.Test;