From b9fcfea67f915ac5acce12d5a0c74c886195d110 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 3 Mar 2026 11:37:12 +0000 Subject: [PATCH 01/46] Add Context Debugger for Variables --- client/src/lsp/client.ts | 8 +- client/src/services/autocomplete.ts | 22 ++-- client/src/services/context.ts | 104 ++++++++++++++---- client/src/services/events.ts | 35 ++++-- client/src/services/state-machine.ts | 4 +- client/src/services/webview.ts | 5 +- client/src/state.ts | 9 +- client/src/types/context.ts | 20 ++-- client/src/types/fsm.ts | 2 +- client/src/webview/diagram.ts | 4 +- client/src/webview/provider.ts | 4 +- client/src/webview/script.ts | 68 +++++++----- client/src/webview/views/context/context.ts | 61 ++++++++++ .../derivation-nodes.ts | 0 .../diagnostics.ts} | 7 +- .../{verification => diagnostics}/errors.ts | 0 .../{verification => diagnostics}/warnings.ts | 0 .../webview/views/{diagram.ts => fsm/fsm.ts} | 9 +- client/src/webview/views/sections.ts | 47 ++++---- .../src/main/java/LJDiagnosticsHandler.java | 7 +- .../java/dtos/diagnostics/SourceRangeDTO.java | 14 +++ .../dtos/errors/ArgumentMismatchErrorDTO.java | 6 +- .../main/java/dtos/errors/CustomErrorDTO.java | 6 +- .../IllegalConstructorTransitionErrorDTO.java | 6 +- .../errors/InvalidRefinementErrorDTO.java | 6 +- .../src/main/java/dtos/errors/LJErrorDTO.java | 6 +- .../java/dtos/errors/NotFoundErrorDTO.java | 6 +- .../java/dtos/errors/RefinementErrorDTO.java | 6 +- .../dtos/errors/StateConflictErrorDTO.java | 6 +- .../dtos/errors/StateRefinementErrorDTO.java | 6 +- .../main/java/dtos/errors/SyntaxErrorDTO.java | 6 +- 31 files changed, 330 insertions(+), 160 deletions(-) create mode 100644 client/src/webview/views/context/context.ts rename client/src/webview/views/{verification => diagnostics}/derivation-nodes.ts (100%) rename client/src/webview/views/{verification/verification.ts => diagnostics/diagnostics.ts} (91%) rename client/src/webview/views/{verification => diagnostics}/errors.ts (100%) rename client/src/webview/views/{verification => diagnostics}/warnings.ts (100%) rename client/src/webview/views/{diagram.ts => fsm/fsm.ts} (83%) create mode 100644 server/src/main/java/dtos/diagnostics/SourceRangeDTO.java diff --git a/client/src/lsp/client.ts b/client/src/lsp/client.ts index 7ffbf69..d01bdc0 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, varsInScope: [], allVars: []}); }); const editor = vscode.window.activeTextEditor; diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 1b3d0d1..1ac7450 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -1,8 +1,7 @@ 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"; type CompletionItemOptions = { @@ -19,20 +18,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(); items.forEach(item => { const label = typeof item.label === "string" ? item.label : item.label.label; @@ -44,7 +43,7 @@ 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 !== "("; if (isDotTrigger) { if (receiver === "this" || receiver === "old(this)") { @@ -52,10 +51,9 @@ function getContextCompletionItems(context: ContextHistory, file: string, annota } return []; } - const variablesInScope = getVariablesInScope(file, extension.selection); - const inScope = variablesInScope !== null; + const inScope = extension.context.varsInScope !== null; const itemsHandlers: Record vscode.CompletionItem[]> = { - vars: () => getVariableCompletionItems(variablesInScope || []), + vars: () => getVariableCompletionItems(extension.context.varsInScope || []), ghosts: () => getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints), aliases: () => getAliasCompletionItems(context.aliases, triggerParameterHints), keywords: () => getKeywordsCompletionItems(triggerParameterHints, inScope), @@ -75,7 +73,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,7 +89,7 @@ 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})`; @@ -110,7 +108,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..9b7dddf 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -1,18 +1,17 @@ import { extension } from "../state"; -import { ContextHistory, Selection, Variable } from "../types/context"; +import { LJContext, Selection, LJVariable } from "../types/context"; -export function handleContextHistory(contextHistory: ContextHistory) { - extension.contextHistory = contextHistory; +export function handleContext(context: LJContext) { + extension.context = 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 getVariablesInScope(file: string, selection: Selection): LJVariable[] | null { // get variables in file - const fileVars = extension.contextHistory.vars[file]; + const fileVars = extension.context.vars[file]; if (!fileVars) return null; + const normalizedSelection = normalizeSelection(selection); // get variables in the current scope based on the selection let mostSpecificScope: string | null = null; @@ -21,7 +20,7 @@ export function getVariablesInScope(file: string, selection: Selection): Variabl // find the most specific scope that contains the selection for (const scope of Object.keys(fileVars)) { const scopeSelection = parseScopeString(scope); - if (isSelectionWithinScope(selection, scopeSelection)) { + if (isSelectionWithinAnother(normalizedSelection, scopeSelection)) { const scopeSize = (scopeSelection.endLine - scopeSelection.startLine) * 10000 + (scopeSelection.endColumn - scopeSelection.startColumn); if (scopeSize < minScopeSize) { mostSpecificScope = scope; @@ -34,8 +33,24 @@ export function getVariablesInScope(file: string, selection: Selection): Variabl // 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#")); + const reachableVariables = getVisibleVariables(variablesInScope, file, normalizedSelection); + const visibleVariables = reachableVariables.filter(v => !v.name.includes("this#")); + return visibleVariables; +} + +function normalizeSelection(selection: Selection): Selection { + const startsBeforeEnds = + selection.startLine < selection.endLine || + (selection.startLine === selection.endLine && selection.startColumn <= selection.endColumn); + + if (startsBeforeEnds) return selection; + + return { + startLine: selection.endLine, + startColumn: selection.endColumn, + endLine: selection.startLine, + endColumn: selection.startColumn, + }; } function parseScopeString(scope: string): Selection { @@ -45,21 +60,68 @@ function parseScopeString(scope: string): Selection { return { startLine, startColumn, endLine, endColumn }; } -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 isSelectionWithinAnother(selection: Selection, another: Selection): boolean { + const startsWithin = selection.startLine > another.startLine || + (selection.startLine === another.startLine && selection.startColumn >= another.startColumn); + const endsWithin = selection.endLine < another.endLine || + (selection.endLine === another.endLine && selection.endColumn <= another.endColumn); return startsWithin && endsWithin; } -function getReachableVariables(variables: Variable[], selection: Selection): Variable[] { +export function filterAndSortVariables(variables: LJVariable[]): LJVariable[] { + // remove duplicates + const uniqueVariables: Map = new Map(); + for (const variable of variables) { + if (!uniqueVariables.has(variable.name)) { + uniqueVariables.set(variable.name, variable); + } + } + // sort by position in code (if available) and then by name + return Array.from(uniqueVariables.values()).sort((left, right) => { + const leftPosition = left.placementInCode?.position + const rightPosition = right.placementInCode?.position + + if (!leftPosition && !rightPosition) return compareVariableNames(left, right); + if (!leftPosition) return 1; + if (!rightPosition) return -1; + if (leftPosition.line !== rightPosition.line) return leftPosition.line - rightPosition.line; + if (leftPosition.column !== rightPosition.column) return leftPosition.column - rightPosition.column; + + return compareVariableNames(left, right); + }); +} + +function compareVariableNames(a: LJVariable, b: LJVariable): number { + return normalizeVariableName(a.name).localeCompare(normalizeVariableName(b.name)); +} + +function normalizeVariableName(name: string): string { + return name.startsWith("#") ? name.split("#")[1] : name; +} + +export function getVisibleVariables(variables: LJVariable[], file: string, selection: Selection, useAnnotationPositions: boolean = false): LJVariable[] { + const isCollapsedSelection = + selection.startLine === selection.endLine && + selection.startColumn === selection.endColumn; + return variables.filter((variable) => { + if (variable.placementInCode?.position.file !== file) return false; // variable is not in the current file + 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; + + // single point cursor + if (isCollapsedSelection) { + const position = useAnnotationPositions ? variable.annPosition || placement : placement; + if (!position || 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 ( + position.line < selection.startLine || + (position.line === selection.startLine && position.column + 1 <= selection.startColumn) + ); + } + // range selection, filter variables that are only within the selection + const varSelection: Selection = { startLine: placement.line, startColumn: placement.column, endLine: placement.line, endColumn: placement.column } + return isSelectionWithinAnother(varSelection, selection); }); } \ No newline at end of file diff --git a/client/src/services/events.ts b/client/src/services/events.ts index bc8501b..f4a217d 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -3,9 +3,9 @@ import { extension } from '../state'; import { updateStateMachine } from './state-machine'; import { Selection } from '../types/context'; import { SELECTION_DEBOUNCE_MS } from '../utils/constants'; +import { getVariablesInScope, getVisibleVariables, filterAndSortVariables } from './context'; let selectionTimeout: NodeJS.Timeout | null = null; -let currentSelection: Selection = { startLine: 0, startColumn: 0, endLine: 0, endColumn: 0 }; /** * Initializes file system event listeners @@ -38,23 +38,40 @@ export async function onActiveFileChange(editor: vscode.TextEditor) { extension.file = editor.document.uri.fsPath; extension.webview?.sendMessage({ type: "file", file: extension.file }); await updateStateMachine(editor.document); + updateSelectionAndContext(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 = { +export async function onSelectionChange(event: vscode.TextEditorSelectionChangeEvent) { + // debounce selection changes + if (selectionTimeout) clearTimeout(selectionTimeout); + selectionTimeout = setTimeout(() => { + updateSelectionAndContext(event.selections[0]); + }, SELECTION_DEBOUNCE_MS); +} + +/** + * Updates the current selection and context + * @param selection The new selection + */ +function updateSelectionAndContext(selection: vscode.Selection) { + const selectionStart = selection.start; + const selectionEnd = selection.end; + const currentSelection: Selection = { startLine: selectionStart.line, startColumn: selectionStart.character, endLine: selectionEnd.line, endColumn: selectionEnd.character }; - // debounce selection changes - if (selectionTimeout) clearTimeout(selectionTimeout); - selectionTimeout = setTimeout(() => extension.selection = currentSelection, SELECTION_DEBOUNCE_MS); + if (extension.context && extension.file) { + const variablesInScope = getVariablesInScope(extension.file, currentSelection) || []; + const otherVars = getVisibleVariables([...(extension.context.instanceVars || []), ...(extension.context.globalVars || [])], extension.file, currentSelection); + const allVars = filterAndSortVariables([...variablesInScope, ...otherVars]); + extension.context.varsInScope = variablesInScope || []; + extension.context.allVars = allVars; + 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..e6a5f7d 100644 --- a/client/src/services/webview.ts +++ b/client/src/services/webview.ts @@ -24,8 +24,9 @@ export function registerWebview(context: vscode.ExtensionContext) { 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..4bb357a 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 } from "./types/context"; export class ExtensionState { // server/client state @@ -22,9 +22,8 @@ export class ExtensionState { // application state file?: string; diagnostics?: LJDiagnostic[]; - stateMachine?: StateMachine; - contextHistory?: ContextHistory; - selection?: Selection; + stateMachine?: LJStateMachine; + context?: LJContext; } 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..509e351 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -2,7 +2,7 @@ import { PlacementInCode, SourcePosition } from "./diagnostics"; // Type definitions used for LiquidJava context information -export type Variable = { +export type LJVariable = { name: string; type: string; refinement: string; @@ -12,7 +12,7 @@ export type Variable = { annPosition: SourcePosition | null; } -export type Ghost = { +export type LJGhost = { name: string; qualifiedName: string; returnType: string; @@ -20,19 +20,21 @@ export type Ghost = { refinement: string; } -export type Alias = { +export type LJAlias = { name: string; parameters: string[]; types: string[]; predicate: string; } -export type ContextHistory = { - vars: Record>; // file -> (scope -> variables in scope) - ghosts: Record; // file -> ghosts in file - instanceVars: Variable[]; - globalVars: Variable[]; - aliases: Alias[]; +export type LJContext = { + vars: Record>; // file -> (scope -> variables in scope) + ghosts: Record; // file -> ghosts in file + instanceVars: LJVariable[]; + globalVars: LJVariable[]; + aliases: LJAlias[]; + varsInScope: LJVariable[]; // variables in scope for the current selection + allVars: LJVariable[]; // instance vars + global vars + vars in scope } export type Selection = { 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/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..c621722 100644 --- a/client/src/webview/provider.ts +++ b/client/src/webview/provider.ts @@ -36,9 +36,7 @@ export class LiquidJavaWebviewProvider implements vscode.WebviewViewProvider { 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 position = new vscode.Position(message.line, message.character); const range = new vscode.Range(position, position); editor.selection = new vscode.Selection(position, position); editor.revealRange(range, vscode.TextEditorRevealType.InCenter); diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index dfa4ff8..7137d91 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -1,11 +1,13 @@ -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 { 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 { renderContextView } from "./views/context/context"; /** * Initializes the webview script @@ -19,8 +21,9 @@ export function getScript(vscode: any, document: any, window: any) { let showAllDiagnostics = false; let currentFile: string | undefined; let expandedErrors = new Set(); - 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 = ''; @@ -135,7 +138,9 @@ export function getScript(vscode: any, document: any, window: any) { if (target.classList.contains('nav-tab')) { e.stopPropagation(); const tab = target.getAttribute('data-tab') as NavTab; + console.log('Tab click:', tab); if (tab && tab !== selectedTab) { + console.log('Switching to tab:', tab); selectedTab = tab; updateView(); } @@ -146,20 +151,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; + switch (msg.type) { + case 'diagnostics': + diagnostics = msg.diagnostics as LJDiagnostic[]; updateView(); - return; - } - stateMachine = msg.sm as StateMachine; - updateView(); + break; + case 'file': + currentFile = msg.file; + if (!showAllDiagnostics) updateView(); + break; + case 'fsm': + stateMachine = msg.sm as LJStateMachine | undefined; + updateView(); + break; + case 'context': + context = msg.context as LJContext; + updateView(); + break; } }); @@ -167,13 +175,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); + break; } } } diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts new file mode 100644 index 0000000..536ad7d --- /dev/null +++ b/client/src/webview/views/context/context.ts @@ -0,0 +1,61 @@ +import { LJContext } from "../../../types/context"; +import { renderLocationLink, renderMainHeader } from "../sections"; + +export function renderContextView(context: LJContext, currentFile: string): string { + if (!context || !currentFile) return ""; + + const varsInScope = context.allVars || []; + const ghosts = context.ghosts[currentFile] || []; + const aliases = context.aliases || []; + const total = varsInScope.length + ghosts.length + aliases.length; + return /*html*/` +
+ ${renderMainHeader("", 'context')} + ${total === 0 ? '

No context information available for the current position.

' : ''} + +
+

Variables in Scope

+
+ ${varsInScope.length > 0 ? /*html*/` + + + + + + + + + + ${varsInScope.map(variable => /*html*/` + + + + + + `).join('')} + +
VariableRefinementLocation
${variable.type} ${variable.name}${variable.refinement}${renderLocationLink(variable.placementInCode.position)}
+ `: '

No variables available in the current position.

'} +
+ + +
+ `; +} + + // ${ghosts.length > 0 ? /*html*/` +//
+//

Ghosts

+//
    +// ${ghosts.map(ghost => /*html*/`
  • ${ghost.name}
    • `).join('')} +//
+//
+// ` : ''} +// ${aliases.length > 0 ? /*html*/` +//
+//

Aliases

+//
    +// ${aliases.map(alias => /*html*/`
  • ${alias.name}
    • `).join('')} +//
+//
+// ` : ''} \ 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 100% rename from client/src/webview/views/verification/derivation-nodes.ts rename to client/src/webview/views/diagnostics/derivation-nodes.ts 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, - 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*/`
- ${renderMainHeader(titleMessage, selectedTab)} + ${renderMainHeader(titleMessage, 'diagnostics')}

${infoMessage}

${ diagnostics.length === 0 ? '' : /*html*/` diff --git a/client/src/webview/views/verification/errors.ts b/client/src/webview/views/diagnostics/errors.ts similarity index 100% rename from client/src/webview/views/verification/errors.ts rename to client/src/webview/views/diagnostics/errors.ts diff --git a/client/src/webview/views/verification/warnings.ts b/client/src/webview/views/diagnostics/warnings.ts similarity index 100% rename from client/src/webview/views/verification/warnings.ts rename to client/src/webview/views/diagnostics/warnings.ts 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..e92bf77 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, type NavTab } 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*/`
- ${renderMainHeader("", selectedTab)} + ${renderMainHeader("", 'fsm')} ${sm ? /*html*/`
-
diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 5e184c1..493318c 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, SourcePosition, TranslationTable } from "../../types/diagnostics"; export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
@@ -17,12 +17,13 @@ export const renderHeader = (diagnostic: LJDiagnostic): string => /*html*/ `

${diagnostic.title}

${diagnostic.message}

`; 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*/`${simpleFile}:${line}`; - return renderCustomSection("Location", /*html*/`
${link}
`); + if (!diagnostic.position || !diagnostic.file) return ""; + const position: SourcePosition = { + file: diagnostic.file, + line: diagnostic.position.lineStart, + column: diagnostic.position.colStart + } + return renderCustomSection("Location", /*html*/`
${renderLocationLink(position)}
`); }; export function renderTranslationTable(translationTable: TranslationTable): string { @@ -42,22 +43,11 @@ export function renderTranslationTable(translationTable: TranslationTable): stri ${entries.map(([variable, placement]: [string, any]) => { - const simpleFile = placement.position.file.split('/').pop() || placement.position.file; - const link = - /*html*/` - ${simpleFile}:${placement.position.line} - `; return /*html*/` ${variable} ${placement.text} - ${link} + ${renderLocationLink(placement.position)} `; }).join('')} @@ -67,14 +57,27 @@ export function renderTranslationTable(translationTable: TranslationTable): stri `; } -export type NavTab = 'verification' | 'state-machine'; +export function renderLocationLink(position?: SourcePosition): string { + if (!position) return 'No location'; + const file = `${position.file.split('/').pop().trim() || position.file}:${position.line}`; + return /*html*/`${file}`; +} + +export type NavTab = 'diagnostics' | 'fsm' | 'context'; export function renderNav(selectedTab: NavTab): string { return /*html*/` `; diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java index ca6902c..4b80432 100644 --- a/server/src/main/java/LJDiagnosticsHandler.java +++ b/server/src/main/java/LJDiagnosticsHandler.java @@ -10,6 +10,7 @@ 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; @@ -107,7 +108,9 @@ private static Range getRangeFromErrorPosition(ErrorPosition pos) { // 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.lineStart() - 1, pos.colStart() - 1), + new Position(pos.lineEnd() - 1, pos.colEnd() - 1) + ); } } diff --git a/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java b/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java new file mode 100644 index 0000000..6b25880 --- /dev/null +++ b/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java @@ -0,0 +1,14 @@ +package dtos.diagnostics; + +import liquidjava.diagnostics.ErrorPosition; + +public record SourceRangeDTO(int lineStart, int colStart, int lineEnd, int colEnd) { + + public static SourceRangeDTO from(ErrorPosition pos) { + if (pos == null) { + // no location information available + return new SourceRangeDTO(0, 0, 0, 0); + } + return new SourceRangeDTO(pos.lineStart() - 1, pos.colStart() - 1, pos.lineEnd() - 1, pos.colEnd() - 1); + } +} diff --git a/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java b/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java index facff9f..ebd16e5 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.SourceRangeDTO; 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) { + SourceRangeDTO position) { public static ArgumentMismatchErrorDTO from(ArgumentMismatchError error) { return new ArgumentMismatchErrorDTO("error", "argument-mismatch-error", error.getTitle(), error.getMessage(), error.getFile(), - error.getPosition()); + SourceRangeDTO.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..510f481 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.SourceRangeDTO; 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, SourceRangeDTO position) { public static CustomErrorDTO from(CustomError error) { return new CustomErrorDTO("error", "custom-error", error.getTitle(), error.getMessage(), error.getFile(), - error.getPosition()); + SourceRangeDTO.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..d65c195 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.SourceRangeDTO; 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) { + SourceRangeDTO position) { public static IllegalConstructorTransitionErrorDTO from(IllegalConstructorTransitionError error) { return new IllegalConstructorTransitionErrorDTO("error", "illegal-constructor-transition-error", error.getTitle(), error.getMessage(), error.getFile(), - error.getPosition()); + SourceRangeDTO.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..0c4d465 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.SourceRangeDTO; 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) { + SourceRangeDTO 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()); + SourceRangeDTO.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..8148da4 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.SourceRangeDTO; 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, SourceRangeDTO position, TranslationTableDTO translationTable) { public static LJErrorDTO from(LJError error) { return new LJErrorDTO(error.getTitle(), error.getMessage(), error.getFile(), - error.getPosition(), TranslationTableDTO.from(error.getTranslationTable())); + SourceRangeDTO.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..6fdce32 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.SourceRangeDTO; 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, SourceRangeDTO 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()); + SourceRangeDTO.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..641ed5f 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.SourceRangeDTO; 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, SourceRangeDTO 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()); + SourceRangeDTO.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..e81487e 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.SourceRangeDTO; 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, SourceRangeDTO 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()); + SourceRangeDTO.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..ca1a416 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.SourceRangeDTO; 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, SourceRangeDTO 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(), + SourceRangeDTO.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..c28d2cf 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.SourceRangeDTO; 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, SourceRangeDTO 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()); + SourceRangeDTO.from(error.getPosition()), error.getRefinement()); } } From a35920fe0d830dcec3b0646836aeec1036c9656c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 3 Mar 2026 13:51:20 +0000 Subject: [PATCH 02/46] Add Ghosts & Aliases to Context Debugger --- client/src/services/autocomplete.ts | 3 +- client/src/services/context.ts | 2 +- client/src/types/context.ts | 1 + client/src/webview/script.ts | 37 ++++++++++- client/src/webview/styles.ts | 30 +++++++++ client/src/webview/utils.ts | 5 ++ client/src/webview/views/context/aliases.ts | 35 ++++++++++ client/src/webview/views/context/context.ts | 64 +++++-------------- client/src/webview/views/context/ghosts.ts | 32 ++++++++++ client/src/webview/views/context/variables.ts | 32 ++++++++++ .../src/webview/views/diagnostics/errors.ts | 4 +- .../src/webview/views/diagnostics/warnings.ts | 4 +- client/src/webview/views/sections.ts | 11 +++- .../src/main/java/dtos/context/GhostDTO.java | 12 +++- 14 files changed, 211 insertions(+), 61 deletions(-) create mode 100644 client/src/webview/utils.ts create mode 100644 client/src/webview/views/context/aliases.ts create mode 100644 client/src/webview/views/context/ghosts.ts create mode 100644 client/src/webview/views/context/variables.ts diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 1ac7450..e34c536 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -93,8 +93,7 @@ function getGhostCompletionItems(ghosts: LJGhost[], triggerParameterHints: boole 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, diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 9b7dddf..351aad6 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -117,7 +117,7 @@ export function getVisibleVariables(variables: LJVariable[], file: string, selec // variable was declared before the cursor line or its in the same line but before the cursor column return ( position.line < selection.startLine || - (position.line === selection.startLine && position.column + 1 <= selection.startColumn) + (position.line === selection.startLine && position.column <= selection.startColumn) ); } // range selection, filter variables that are only within the selection diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 509e351..1e06e4b 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -18,6 +18,7 @@ export type LJGhost = { returnType: string; parameterTypes: string[]; refinement: string; + isState: boolean; } export type LJAlias = { diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 7137d91..f21c6f9 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -7,7 +7,7 @@ import type { LJStateMachine } from "../types/fsm"; import type { NavTab } from "./views/sections"; import { renderDiagnosticsView } from "./views/diagnostics/diagnostics"; import { LJContext } from "../types/context"; -import { renderContextView } from "./views/context/context"; +import { ContextSectionState, renderContextView } from "./views/context/context"; /** * Initializes the webview script @@ -26,6 +26,11 @@ export function getScript(vscode: any, document: any, window: any) { let selectedTab: NavTab = 'diagnostics'; let diagramOrientation: "LR" | "TB" = "TB"; let currentDiagram: string = ''; + const contextSectionState: ContextSectionState = { + vars: true, + ghosts: true, + aliases: true, + }; // initial state root.innerHTML = renderLoading(); @@ -36,6 +41,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(); @@ -186,7 +219,7 @@ export function getScript(vscode: any, document: any, window: any) { if (stateMachine) renderMermaidDiagram(document, window); break; case 'context': - root.innerHTML = renderContextView(context, currentFile); + root.innerHTML = renderContextView(context, currentFile, contextSectionState); break; } } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index f4d5797..53976bb 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -288,6 +288,36 @@ export function getStyles(): string { font-family: var(--vscode-editor-font-family); font-size: 0.9em; } + .context-section { + margin-bottom: 1rem; + } + .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; + } .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..2059194 --- /dev/null +++ b/client/src/webview/utils.ts @@ -0,0 +1,5 @@ + +export function getSimpleName(qualifiedName: string): string { + const parts = qualifiedName.split('.'); + return parts[parts.length - 1]; +} \ 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..01a638e --- /dev/null +++ b/client/src/webview/views/context/aliases.ts @@ -0,0 +1,35 @@ +import { LJAlias } from "../../../types/context"; +import { getSimpleName } from "../../utils"; +import { renderToggleSection } from "../sections"; + +export function renderContextAliases(aliases: LJAlias[], isExpanded: boolean): string { + return /*html*/` +
+ ${renderToggleSection('Aliases', 'context-aliases', isExpanded)} +
+ ${aliases.length > 0 ? /*html*/` + + + + + + + + + ${aliases.map(alias => /*html*/` + + + + + `).join('')} + +
NamePredicate
+ + ${alias.name}(${alias.parameters.map((parameter, index) => `${getSimpleName(alias.types[index])} ${parameter}`).join(", ")}) + + ${alias.predicate}
+ ` : '

No aliases available in the current file.

'} +
+
+ `; +} \ No newline at end of file diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index 536ad7d..c79f328 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -1,61 +1,29 @@ import { LJContext } from "../../../types/context"; -import { renderLocationLink, renderMainHeader } from "../sections"; +import { renderMainHeader } from "../sections"; +import { renderContextAliases } from "./aliases"; +import { renderContextGhosts } from "./ghosts"; +import { renderContextVariables } from "./variables"; -export function renderContextView(context: LJContext, currentFile: string): string { +export type ContextSectionState = { + vars: boolean; + ghosts: boolean; + aliases: boolean; +} + +export function renderContextView(context: LJContext, currentFile: string, sectionState: ContextSectionState): string { if (!context || !currentFile) return ""; - const varsInScope = context.allVars || []; + const allVars = context.allVars || []; const ghosts = context.ghosts[currentFile] || []; const aliases = context.aliases || []; - const total = varsInScope.length + ghosts.length + aliases.length; + const total = allVars.length + ghosts.length + aliases.length; return /*html*/`
${renderMainHeader("", 'context')} ${total === 0 ? '

No context information available for the current position.

' : ''} - -
-

Variables in Scope

-
- ${varsInScope.length > 0 ? /*html*/` - - - - - - - - - - ${varsInScope.map(variable => /*html*/` - - - - - - `).join('')} - -
VariableRefinementLocation
${variable.type} ${variable.name}${variable.refinement}${renderLocationLink(variable.placementInCode.position)}
- `: '

No variables available in the current position.

'} -
- - + ${renderContextAliases(aliases, sectionState.aliases)} + ${renderContextGhosts(ghosts, sectionState.ghosts)} + ${renderContextVariables(allVars, sectionState.vars)}
`; } - - // ${ghosts.length > 0 ? /*html*/` -//
-//

Ghosts

-//
    -// ${ghosts.map(ghost => /*html*/`
  • ${ghost.name}
    • `).join('')} -//
-//
-// ` : ''} -// ${aliases.length > 0 ? /*html*/` -//
-//

Aliases

-//
    -// ${aliases.map(alias => /*html*/`
  • ${alias.name}
    • `).join('')} -//
-//
-// ` : ''} \ No newline at end of file diff --git a/client/src/webview/views/context/ghosts.ts b/client/src/webview/views/context/ghosts.ts new file mode 100644 index 0000000..a12ebc2 --- /dev/null +++ b/client/src/webview/views/context/ghosts.ts @@ -0,0 +1,32 @@ +import { LJGhost } from "../../../types/context"; +import { renderToggleSection } from "../sections"; + +export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): string { + return /*html*/` +
+ ${renderToggleSection('Ghosts', 'context-ghosts', isExpanded)} +
+ ${ghosts.length > 0 ? /*html*/` + + + + + + + + + + ${ghosts.map(ghost => /*html*/` + + + + + + `).join('')} + +
NameKindParameters
${ghost.returnType} ${ghost.name}${ghost.isState ? 'State' : 'Ghost'}${ghost.parameterTypes.join(', ') || '-'}
+ ` : '

No ghosts available in the current file.

'} +
+
+ `; +} \ 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..974131e --- /dev/null +++ b/client/src/webview/views/context/variables.ts @@ -0,0 +1,32 @@ +import { LJVariable } from "../../../types/context"; +import { renderLocationLink, renderToggleSection } from "../sections"; + +export function renderContextVariables(variables: LJVariable[], isExpanded: boolean): string { + return /*html*/` +
+ ${renderToggleSection('Variables', 'context-vars', isExpanded)} +
+ ${variables.length > 0 ? /*html*/` + + + + + + + + + + ${variables.map(variable => /*html*/` + + + + + + `).join('')} + +
VariableRefinementLocation
${variable.type} ${variable.name}${variable.refinement}${variable.placementInCode ? `${renderLocationLink(variable.placementInCode.position)}` : 'Unknown'}
+ `: '

No variables available in the current position.

'} +
+
+ `; +} \ No newline at end of file diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index 3fcf35f..da3f944 100644 --- a/client/src/webview/views/diagnostics/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 }; 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/diagnostics/warnings.ts b/client/src/webview/views/diagnostics/warnings.ts index 8660467..dde140e 100644 --- a/client/src/webview/views/diagnostics/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 /*ht export const renderSection = (title: string, body: string): string => /*html*/ renderCustomSection(title, `
${body}
`); -export const renderHeader = (diagnostic: LJDiagnostic): string => /*html*/ +export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/` + + `; + +export const renderDiagnosticHeader = (diagnostic: LJDiagnostic): string => /*html*/ `

${diagnostic.title}

${diagnostic.message}

`; export const renderLocation = (diagnostic: LJDiagnostic): string => { @@ -81,4 +88,4 @@ export function renderNav(selectedTab: NavTab): string { `; -} \ No newline at end of file +} diff --git a/server/src/main/java/dtos/context/GhostDTO.java b/server/src/main/java/dtos/context/GhostDTO.java index 968852b..e7521a4 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,22 @@ public record GhostDTO( String qualifiedName, String returnType, List parameterTypes, - String refinement + String refinement, + boolean isState ) { + 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 ); } } \ No newline at end of file From aa6a36e3e83fef90a431e885c6bda86fe57275e1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 3 Mar 2026 13:57:04 +0000 Subject: [PATCH 03/46] Minor Changes --- client/src/webview/script.ts | 6 +++--- client/src/webview/views/context/context.ts | 10 ++++++---- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index f21c6f9..ffe4e3f 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -27,9 +27,9 @@ export function getScript(vscode: any, document: any, window: any) { let diagramOrientation: "LR" | "TB" = "TB"; let currentDiagram: string = ''; const contextSectionState: ContextSectionState = { - vars: true, - ghosts: true, - aliases: true, + vars: false, + ghosts: false, + aliases: false, }; // initial state diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index c79f328..7e29d97 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -20,10 +20,12 @@ export function renderContextView(context: LJContext, currentFile: string, secti return /*html*/`
${renderMainHeader("", 'context')} - ${total === 0 ? '

No context information available for the current position.

' : ''} - ${renderContextAliases(aliases, sectionState.aliases)} - ${renderContextGhosts(ghosts, sectionState.ghosts)} - ${renderContextVariables(allVars, sectionState.vars)} + ${total === 0 + ? '

No context information available for the current position.

' + : `${renderContextAliases(aliases, sectionState.aliases)} + ${renderContextGhosts(ghosts, sectionState.ghosts)} + ${renderContextVariables(allVars, sectionState.vars)} + `}
`; } From 424e48aa3fcedacc91ee16fbce6c9ffe62c23029 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 3 Mar 2026 14:19:16 +0000 Subject: [PATCH 04/46] Filter Instance Variables By Name This is to only show the instance variables that are relevant for the current scope - if there are no variables with the name x, then all variables #x_n should not be shown. However, this is not ideal because we can have variables with the same name. --- client/src/services/context.ts | 4 ++++ client/src/services/events.ts | 10 ++++++---- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 351aad6..5a80824 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -124,4 +124,8 @@ export function getVisibleVariables(variables: LJVariable[], file: string, selec const varSelection: Selection = { startLine: placement.line, startColumn: placement.column, endLine: placement.line, endColumn: placement.column } return isSelectionWithinAnother(varSelection, selection); }); +} + +export function filterInstanceVariables(instanceVars: LJVariable[], variablesInScope: LJVariable[]): LJVariable[] { + return instanceVars.filter(v => variablesInScope.some(s => s.name === v.name.split("_")[0].replace(/^#/, ''))); } \ No newline at end of file diff --git a/client/src/services/events.ts b/client/src/services/events.ts index f4a217d..d906c9e 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -3,7 +3,7 @@ import { extension } from '../state'; import { updateStateMachine } from './state-machine'; import { Selection } from '../types/context'; import { SELECTION_DEBOUNCE_MS } from '../utils/constants'; -import { getVariablesInScope, getVisibleVariables, filterAndSortVariables } from './context'; +import { getVariablesInScope, getVisibleVariables, filterAndSortVariables, filterInstanceVariables } from './context'; let selectionTimeout: NodeJS.Timeout | null = null; @@ -68,9 +68,11 @@ function updateSelectionAndContext(selection: vscode.Selection) { }; if (extension.context && extension.file) { const variablesInScope = getVariablesInScope(extension.file, currentSelection) || []; - const otherVars = getVisibleVariables([...(extension.context.instanceVars || []), ...(extension.context.globalVars || [])], extension.file, currentSelection); - const allVars = filterAndSortVariables([...variablesInScope, ...otherVars]); - extension.context.varsInScope = variablesInScope || []; + const instanceVariables = filterInstanceVariables(extension.context.instanceVars || [], variablesInScope); + const globalVariables = extension.context.globalVars || []; + const visibleInstanceVariables = getVisibleVariables(instanceVariables, extension.file, currentSelection); + const allVars = filterAndSortVariables([...variablesInScope, ...globalVariables, ...visibleInstanceVariables]); + extension.context.varsInScope = variablesInScope; extension.context.allVars = allVars; extension.webview?.sendMessage({ type: "context", context: extension.context }); } From d973d94e0b56cbb2562c3d7cb7bb3d2ad28c88ff Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 3 Mar 2026 14:19:28 +0000 Subject: [PATCH 05/46] Fix Location Line Offset --- client/src/webview/views/sections.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 239cd1c..0198050 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -66,7 +66,7 @@ export function renderTranslationTable(translationTable: TranslationTable): stri export function renderLocationLink(position?: SourcePosition): string { if (!position) return 'No location'; - const file = `${position.file.split('/').pop().trim() || position.file}:${position.line}`; + const file = `${position.file.split('/').pop().trim() || position.file}:${position.line + 1}`; return /*html*/` Date: Tue, 3 Mar 2026 14:37:03 +0000 Subject: [PATCH 06/46] Change Variable Column Offset --- client/src/services/context.ts | 2 +- client/src/webview/views/context/aliases.ts | 2 +- client/src/webview/views/context/ghosts.ts | 2 +- client/src/webview/views/context/variables.ts | 6 +++++- 4 files changed, 8 insertions(+), 4 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 5a80824..d08a7e6 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -117,7 +117,7 @@ export function getVisibleVariables(variables: LJVariable[], file: string, selec // variable was declared before the cursor line or its in the same line but before the cursor column return ( position.line < selection.startLine || - (position.line === selection.startLine && position.column <= selection.startColumn) + (position.line === selection.startLine && position.column + 1 <= selection.startColumn) ); } // range selection, filter variables that are only within the selection diff --git a/client/src/webview/views/context/aliases.ts b/client/src/webview/views/context/aliases.ts index 01a638e..4ab098a 100644 --- a/client/src/webview/views/context/aliases.ts +++ b/client/src/webview/views/context/aliases.ts @@ -11,7 +11,7 @@ export function renderContextAliases(aliases: LJAlias[], isExpanded: boolean): s - + diff --git a/client/src/webview/views/context/ghosts.ts b/client/src/webview/views/context/ghosts.ts index a12ebc2..82901fb 100644 --- a/client/src/webview/views/context/ghosts.ts +++ b/client/src/webview/views/context/ghosts.ts @@ -10,7 +10,7 @@ export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): str
NameAlias Predicate
- + diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 974131e..308dc45 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -20,7 +20,11 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool - + `).join('')} From 0700ae116c6668e7e8028a0b6b570b75f8330a7f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 3 Mar 2026 15:41:26 +0000 Subject: [PATCH 07/46] Code Refactoring --- client/src/services/context.ts | 78 ++++++++++++--------- client/src/services/events.ts | 21 ++---- client/src/webview/script.ts | 4 +- client/src/webview/views/context/context.ts | 4 +- 4 files changed, 57 insertions(+), 50 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index d08a7e6..9ce8afe 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -5,6 +5,16 @@ export function handleContext(context: LJContext) { extension.context = context; } +export function updateContextWithSelection(selection: Selection) { + const variablesInScope = getVariablesInScope(extension.file, selection) || []; + const instanceVariables = filterInstanceVariables(extension.context.instanceVars || [], variablesInScope); + const globalVariables = extension.context.globalVars || []; + const visibleInstanceVariables = getVisibleVariables(instanceVariables, extension.file, selection); + const allVars = sortVariables(filterDuplicateVariables([...variablesInScope, ...globalVariables, ...visibleInstanceVariables])); + extension.context.varsInScope = variablesInScope; + extension.context.allVars = allVars; +} + // 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): LJVariable[] | null { @@ -38,6 +48,34 @@ export function getVariablesInScope(file: string, selection: Selection): LJVaria return visibleVariables; } +function getVisibleVariables(variables: LJVariable[], file: string, selection: Selection, useAnnotationPositions: boolean = false): LJVariable[] { + const isCollapsedSelection = + selection.startLine === selection.endLine && + selection.startColumn === selection.endColumn; + + return variables.filter((variable) => { + if (variable.placementInCode?.position.file !== file) return false; // variable is not in the current file + + const placement = variable.placementInCode?.position; + + // single point cursor + if (isCollapsedSelection) { + const position = useAnnotationPositions ? variable.annPosition || placement : placement; + if (!position || 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 ( + position.line < selection.startLine || + (position.line === selection.startLine && position.column + 1 <= selection.startColumn) + ); + } + // range selection, filter variables that are only within the selection + const varSelection: Selection = { startLine: placement.line, startColumn: placement.column, endLine: placement.line, endColumn: placement.column } + return isSelectionWithinAnother(varSelection, selection); + }); +} + +// Normalizes the selection to ensure start is before end function normalizeSelection(selection: Selection): Selection { const startsBeforeEnds = selection.startLine < selection.endLine || @@ -68,16 +106,19 @@ function isSelectionWithinAnother(selection: Selection, another: Selection): boo return startsWithin && endsWithin; } -export function filterAndSortVariables(variables: LJVariable[]): LJVariable[] { - // remove duplicates +function filterDuplicateVariables(variables: LJVariable[]): LJVariable[] { const uniqueVariables: Map = new Map(); for (const variable of variables) { if (!uniqueVariables.has(variable.name)) { uniqueVariables.set(variable.name, variable); } } - // sort by position in code (if available) and then by name - return Array.from(uniqueVariables.values()).sort((left, right) => { + return Array.from(uniqueVariables.values()); +} + +function sortVariables(variables: LJVariable[]): LJVariable[] { + // sort by position or name + return variables.sort((left, right) => { const leftPosition = left.placementInCode?.position const rightPosition = right.placementInCode?.position @@ -99,33 +140,6 @@ function normalizeVariableName(name: string): string { return name.startsWith("#") ? name.split("#")[1] : name; } -export function getVisibleVariables(variables: LJVariable[], file: string, selection: Selection, useAnnotationPositions: boolean = false): LJVariable[] { - const isCollapsedSelection = - selection.startLine === selection.endLine && - selection.startColumn === selection.endColumn; - - return variables.filter((variable) => { - if (variable.placementInCode?.position.file !== file) return false; // variable is not in the current file - - const placement = variable.placementInCode?.position; - - // single point cursor - if (isCollapsedSelection) { - const position = useAnnotationPositions ? variable.annPosition || placement : placement; - if (!position || 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 ( - position.line < selection.startLine || - (position.line === selection.startLine && position.column + 1 <= selection.startColumn) - ); - } - // range selection, filter variables that are only within the selection - const varSelection: Selection = { startLine: placement.line, startColumn: placement.column, endLine: placement.line, endColumn: placement.column } - return isSelectionWithinAnother(varSelection, selection); - }); -} - -export function filterInstanceVariables(instanceVars: LJVariable[], variablesInScope: LJVariable[]): LJVariable[] { +function filterInstanceVariables(instanceVars: LJVariable[], variablesInScope: LJVariable[]): LJVariable[] { return instanceVars.filter(v => variablesInScope.some(s => s.name === v.name.split("_")[0].replace(/^#/, ''))); } \ No newline at end of file diff --git a/client/src/services/events.ts b/client/src/services/events.ts index d906c9e..feabb84 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -3,7 +3,7 @@ import { extension } from '../state'; import { updateStateMachine } from './state-machine'; import { Selection } from '../types/context'; import { SELECTION_DEBOUNCE_MS } from '../utils/constants'; -import { getVariablesInScope, getVisibleVariables, filterAndSortVariables, filterInstanceVariables } from './context'; +import { updateContextWithSelection } from './context'; let selectionTimeout: NodeJS.Timeout | null = null; @@ -38,7 +38,7 @@ export async function onActiveFileChange(editor: vscode.TextEditor) { extension.file = editor.document.uri.fsPath; extension.webview?.sendMessage({ type: "file", file: extension.file }); await updateStateMachine(editor.document); - updateSelectionAndContext(editor.selection); + handleContextUpdate(editor.selection); } /** @@ -49,7 +49,7 @@ export async function onSelectionChange(event: vscode.TextEditorSelectionChangeE // debounce selection changes if (selectionTimeout) clearTimeout(selectionTimeout); selectionTimeout = setTimeout(() => { - updateSelectionAndContext(event.selections[0]); + handleContextUpdate(event.selections[0]); }, SELECTION_DEBOUNCE_MS); } @@ -57,7 +57,8 @@ export async function onSelectionChange(event: vscode.TextEditorSelectionChangeE * Updates the current selection and context * @param selection The new selection */ -function updateSelectionAndContext(selection: vscode.Selection) { +function handleContextUpdate(selection: vscode.Selection) { + if (!extension.file || !extension.context) return; const selectionStart = selection.start; const selectionEnd = selection.end; const currentSelection: Selection = { @@ -66,14 +67,6 @@ function updateSelectionAndContext(selection: vscode.Selection) { endLine: selectionEnd.line, endColumn: selectionEnd.character }; - if (extension.context && extension.file) { - const variablesInScope = getVariablesInScope(extension.file, currentSelection) || []; - const instanceVariables = filterInstanceVariables(extension.context.instanceVars || [], variablesInScope); - const globalVariables = extension.context.globalVars || []; - const visibleInstanceVariables = getVisibleVariables(instanceVariables, extension.file, currentSelection); - const allVars = filterAndSortVariables([...variablesInScope, ...globalVariables, ...visibleInstanceVariables]); - extension.context.varsInScope = variablesInScope; - extension.context.allVars = allVars; - extension.webview?.sendMessage({ type: "context", context: extension.context }); - } + updateContextWithSelection(currentSelection); + extension.webview?.sendMessage({ type: "context", context: extension.context }); } \ No newline at end of file diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index ffe4e3f..4cbaf7d 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -27,9 +27,9 @@ export function getScript(vscode: any, document: any, window: any) { let diagramOrientation: "LR" | "TB" = "TB"; let currentDiagram: string = ''; const contextSectionState: ContextSectionState = { - vars: false, - ghosts: false, aliases: false, + ghosts: false, + vars: true, }; // initial state diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index 7e29d97..fd328ba 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -5,9 +5,9 @@ import { renderContextGhosts } from "./ghosts"; import { renderContextVariables } from "./variables"; export type ContextSectionState = { - vars: boolean; - ghosts: boolean; aliases: boolean; + ghosts: boolean; + vars: boolean; } export function renderContextView(context: LJContext, currentFile: string, sectionState: ContextSectionState): string { From 6ea0524ca3bccc483d5c803c4d73d79a93633929 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 3 Mar 2026 20:38:32 +0000 Subject: [PATCH 08/46] Add Variable Highlighting --- client/src/services/context.ts | 3 +- client/src/services/highlight.ts | 19 +++++++++++ client/src/utils/utils.ts | 4 +++ client/src/webview/provider.ts | 4 +++ client/src/webview/script.ts | 28 ++++++++++++++- client/src/webview/styles.ts | 11 ++++++ client/src/webview/utils.ts | 4 +++ client/src/webview/views/context/aliases.ts | 10 ++---- client/src/webview/views/context/ghosts.ts | 13 ++----- client/src/webview/views/context/variables.ts | 34 ++++++++++--------- 10 files changed, 94 insertions(+), 36 deletions(-) create mode 100644 client/src/services/highlight.ts diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 9ce8afe..09715d4 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -1,5 +1,6 @@ import { extension } from "../state"; import { LJContext, Selection, LJVariable } from "../types/context"; +import { getOriginalVariableName } from "../utils/utils"; export function handleContext(context: LJContext) { extension.context = context; @@ -141,5 +142,5 @@ function normalizeVariableName(name: string): string { } function filterInstanceVariables(instanceVars: LJVariable[], variablesInScope: LJVariable[]): LJVariable[] { - return instanceVars.filter(v => variablesInScope.some(s => s.name === v.name.split("_")[0].replace(/^#/, ''))); + return instanceVars.filter(v => variablesInScope.some(s => s.name === getOriginalVariableName(v.name))); } \ No newline at end of file diff --git a/client/src/services/highlight.ts b/client/src/services/highlight.ts new file mode 100644 index 0000000..990133c --- /dev/null +++ b/client/src/services/highlight.ts @@ -0,0 +1,19 @@ +import * as vscode from 'vscode' +import { Selection } from '../types/context' + +const highlight = vscode.window.createTextEditorDecorationType({ + backgroundColor: 'rgba(255, 255, 0, 0.3)' +}) + +export function highlightRange(editor: vscode.TextEditor, selection: Selection) { + if (!selection) { + editor.setDecorations(highlight, []); + return; + } + const range = new vscode.Range( + new vscode.Position(selection.startLine, selection.startColumn), + new vscode.Position(selection.endLine, selection.endColumn) + ) + editor.setDecorations(highlight, [{ range }]) + editor.revealRange(range, vscode.TextEditorRevealType.InCenter) +} \ No newline at end of file diff --git a/client/src/utils/utils.ts b/client/src/utils/utils.ts index e0eb229..305e775 100644 --- a/client/src/utils/utils.ts +++ b/client/src/utils/utils.ts @@ -127,4 +127,8 @@ 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(/^#/, ''); } \ No newline at end of file diff --git a/client/src/webview/provider.ts b/client/src/webview/provider.ts index c621722..38a3179 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 } from '../services/highlight'; /** * Webview provider for the LiquidJava extension @@ -42,6 +43,9 @@ export class LiquidJavaWebviewProvider implements vscode.WebviewViewProvider { editor.revealRange(range, vscode.TextEditorRevealType.InCenter); }); }); + } else if (message.type === "highlight") { + // highlight the specified range in the current editor + highlightRange(vscode.window.activeTextEditor, message.selection); } }); } diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 4cbaf7d..7bcfc0e 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -6,7 +6,7 @@ import type { LJDiagnostic } from "../types/diagnostics"; import type { LJStateMachine } from "../types/fsm"; import type { NavTab } from "./views/sections"; import { renderDiagnosticsView } from "./views/diagnostics/diagnostics"; -import { LJContext } from "../types/context"; +import { LJContext, Selection } from "../types/context"; import { ContextSectionState, renderContextView } from "./views/context/context"; /** @@ -167,6 +167,32 @@ export function getScript(vscode: any, document: any, window: any) { return; } + // highlight variable + if (target.classList.contains('highlight-btn')) { + e.stopPropagation(); + + const previousSelected = root.querySelector('.highlight-btn.selected'); + if (previousSelected) { + // unselect previous + previousSelected.classList.remove('selected'); + if (previousSelected === target) { + // remove highlight + vscode.postMessage({ type: 'highlight', selection: null }); + return; + } + } + target.classList.add('selected'); + + const startLine = parseInt(target.getAttribute('data-start-line') || '', 10); + const startColumn = parseInt(target.getAttribute('data-start-column') || '', 10); + const endLine = parseInt(target.getAttribute('data-end-line') || '', 10); + const endColumn = parseInt(target.getAttribute('data-end-column') || '', 10); + if ([startLine, startColumn, endLine, endColumn].some(Number.isNaN)) return; + const selection: Selection = { startLine, startColumn, endLine, endColumn }; + vscode.postMessage({ type: 'highlight', selection }); + return; + } + // nav tab click if (target.classList.contains('nav-tab')) { e.stopPropagation(); diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 53976bb..c1b5b7e 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -318,6 +318,17 @@ export function getStyles(): string { .context-section-content.collapsed { display: none; } + .highlight-btn { + background-color: transparent; + border: none; + transition: background-color 0.1s; + } + .highlight-btn code { + pointer-events: none; + } + .highlight-btn.selected { + background-color: var(--vscode-button-background); + } .diagram-section { margin-bottom: 1.5rem; padding-bottom: 1rem; diff --git a/client/src/webview/utils.ts b/client/src/webview/utils.ts index 2059194..2e0fa36 100644 --- a/client/src/webview/utils.ts +++ b/client/src/webview/utils.ts @@ -2,4 +2,8 @@ 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(/^#/, ''); } \ No newline at end of file diff --git a/client/src/webview/views/context/aliases.ts b/client/src/webview/views/context/aliases.ts index 4ab098a..45c6697 100644 --- a/client/src/webview/views/context/aliases.ts +++ b/client/src/webview/views/context/aliases.ts @@ -9,21 +9,15 @@ export function renderContextAliases(aliases: LJAlias[], isExpanded: boolean): s
${aliases.length > 0 ? /*html*/`
NameGhost Kind Parameters
${variable.type} ${variable.name} ${variable.refinement}${variable.placementInCode ? `${renderLocationLink(variable.placementInCode.position)}` : 'Unknown'} + ${variable.placementInCode + ?`${renderLocationLink({ ...variable.placementInCode.position, column: variable.placementInCode.position.column + 1 })}` + : 'Unknown'} +
- - - - - - ${aliases.map(alias => /*html*/` - + `).join('')} diff --git a/client/src/webview/views/context/ghosts.ts b/client/src/webview/views/context/ghosts.ts index 82901fb..ab68371 100644 --- a/client/src/webview/views/context/ghosts.ts +++ b/client/src/webview/views/context/ghosts.ts @@ -1,4 +1,5 @@ import { LJGhost } from "../../../types/context"; +import { getSimpleName } from "../../utils"; import { renderToggleSection } from "../sections"; export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): string { @@ -8,19 +9,11 @@ export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): str
${ghosts.length > 0 ? /*html*/`
AliasPredicate
- ${alias.name}(${alias.parameters.map((parameter, index) => `${getSimpleName(alias.types[index])} ${parameter}`).join(", ")}) + ${alias.name}(${alias.parameters.map((parameter, index) => `${getSimpleName(alias.types[index])} ${parameter}`).join(", ")}) { ${alias.predicate} } ${alias.predicate}alias
- - - - - - - ${ghosts.map(ghost => /*html*/` - - - + + `).join('')} diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 308dc45..1507988 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -1,5 +1,6 @@ import { LJVariable } from "../../../types/context"; -import { renderLocationLink, renderToggleSection } from "../sections"; +import { getOriginalVariableName } from "../../utils"; +import { renderToggleSection } from "../sections"; export function renderContextVariables(variables: LJVariable[], isExpanded: boolean): string { return /*html*/` @@ -8,23 +9,11 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool
${variables.length > 0 ? /*html*/`
GhostKindParameters
${ghost.returnType} ${ghost.name}${ghost.isState ? 'State' : 'Ghost'}${ghost.parameterTypes.join(', ') || '-'}${ghost.returnType} ${ghost.name}(${ghost.parameterTypes.map(getSimpleName).join(', ')})${ghost.isState ? 'state' : 'ghost'}
- - - - - - - ${variables.map(variable => /*html*/` - - - + + `).join('')} @@ -33,4 +22,17 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool `; -} \ No newline at end of file +} + +function renderVariable(variable: LJVariable): string { + const position = variable.placementInCode.position; + const variableName = getOriginalVariableName(variable.name); + return /*html*/` + `; +} From 31d960bef2114334a028b58e0413710304f2d9d8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 4 Mar 2026 17:48:57 +0000 Subject: [PATCH 09/46] Handle Edge Cases Refinements with `true` and return variables --- client/src/services/context.ts | 8 +++----- client/src/webview/views/context/variables.ts | 6 ++++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 09715d4..247a693 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -126,6 +126,8 @@ function sortVariables(variables: LJVariable[]): LJVariable[] { if (!leftPosition && !rightPosition) return compareVariableNames(left, right); if (!leftPosition) return 1; if (!rightPosition) return -1; + if (getOriginalVariableName(left.name) === "ret") return 1; + if (getOriginalVariableName(right.name) === "ret") return -1; if (leftPosition.line !== rightPosition.line) return leftPosition.line - rightPosition.line; if (leftPosition.column !== rightPosition.column) return leftPosition.column - rightPosition.column; @@ -134,11 +136,7 @@ function sortVariables(variables: LJVariable[]): LJVariable[] { } function compareVariableNames(a: LJVariable, b: LJVariable): number { - return normalizeVariableName(a.name).localeCompare(normalizeVariableName(b.name)); -} - -function normalizeVariableName(name: string): string { - return name.startsWith("#") ? name.split("#")[1] : name; + return getOriginalVariableName(a.name).localeCompare(getOriginalVariableName(b.name)); } function filterInstanceVariables(instanceVars: LJVariable[], variablesInScope: LJVariable[]): LJVariable[] { diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 1507988..20b5e52 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -25,8 +25,9 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool } function renderVariable(variable: LJVariable): string { - const position = variable.placementInCode.position; const variableName = getOriginalVariableName(variable.name); + const refinement = variable.refinement !== "true" ? variable.refinement.replace("==", "=") : variable.name + const position = variable.placementInCode.position; // TODO: handle cases where we don't really have the correct position for the variable return /*html*/` `; + ${variableName === "ret" ? 'disabled' : ''} + >${refinement}`; } From 22a14f26242113e54a7645a9a30c82a8874830b3 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Mar 2026 16:03:31 +0000 Subject: [PATCH 10/46] Show Failed Refinements --- client/src/types/context.ts | 1 + client/src/webview/script.ts | 4 ++-- client/src/webview/styles.ts | 11 +++++++--- client/src/webview/views/context/variables.ts | 20 +++++++++++-------- client/src/webview/views/sections.ts | 2 +- .../main/java/dtos/context/VariableDTO.java | 6 ++++-- 6 files changed, 28 insertions(+), 16 deletions(-) diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 1e06e4b..401f913 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -10,6 +10,7 @@ export type LJVariable = { placementInCode: PlacementInCode | null; isParameter: boolean; annPosition: SourcePosition | null; + failingRefinement: string | null; } export type LJGhost = { diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 7bcfc0e..a1f7ff4 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -168,10 +168,10 @@ export function getScript(vscode: any, document: any, window: any) { } // highlight variable - if (target.classList.contains('highlight-btn')) { + if (target.classList.contains('context-variable-btn')) { e.stopPropagation(); - const previousSelected = root.querySelector('.highlight-btn.selected'); + const previousSelected = root.querySelector('.context-variable-btn.selected'); if (previousSelected) { // unselect previous previousSelected.classList.remove('selected'); diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index c1b5b7e..13e43a6 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -318,17 +318,22 @@ export function getStyles(): string { .context-section-content.collapsed { display: none; } - .highlight-btn { + .context-variable-btn { background-color: transparent; border: none; transition: background-color 0.1s; } - .highlight-btn code { + .context-variable-btn code { pointer-events: none; } - .highlight-btn.selected { + .context-variable-btn.selected { background-color: var(--vscode-button-background); } + .context-variable .failing-refinement { + color: var(--vscode-editorError-foreground); + font-size: 0.9rem; + margin-left: 0.25rem; + } .diagram-section { margin-bottom: 1.5rem; padding-bottom: 1rem; diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 20b5e52..59052a7 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -29,12 +29,16 @@ function renderVariable(variable: LJVariable): string { const refinement = variable.refinement !== "true" ? variable.refinement.replace("==", "=") : variable.name const position = variable.placementInCode.position; // TODO: handle cases where we don't really have the correct position for the variable return /*html*/` - `; +
+ + ${variable.failingRefinement ? /*html*/`⊢ ${variable.failingRefinement}` : ''} +
`; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 0198050..6687473 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -83,8 +83,8 @@ export function renderNav(selectedTab: NavTab): string { `; diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index f89148e..dbecebd 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -14,7 +14,8 @@ public record VariableDTO( String mainRefinement, PlacementInCodeDTO placementInCode, boolean isParameter, - SourcePositionDTO annPosition + SourcePositionDTO annPosition, + String failingRefinement ) { public static VariableDTO from(RefinedVariable refinedVariable) { return new VariableDTO( @@ -24,7 +25,8 @@ public static VariableDTO from(RefinedVariable refinedVariable) { refinedVariable.getMainRefinement().toString(), PlacementInCodeDTO.from(refinedVariable.getPlacementInCode()), refinedVariable.isParameter(), - SourcePositionDTO.from(refinedVariable.getAnnPosition()) + SourcePositionDTO.from(refinedVariable.getAnnPosition()), + refinedVariable.getFailingRefinement() != null ? refinedVariable.getFailingRefinement().toString() : null ); } } \ No newline at end of file From dfe76abbd965f8ad6f7e617067811c135bc82bbb Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Mar 2026 16:54:19 +0000 Subject: [PATCH 11/46] Update Styling --- client/src/webview/styles.ts | 1 - 1 file changed, 1 deletion(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 13e43a6..ba0b455 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -332,7 +332,6 @@ export function getStyles(): string { .context-variable .failing-refinement { color: var(--vscode-editorError-foreground); font-size: 0.9rem; - margin-left: 0.25rem; } .diagram-section { margin-bottom: 1.5rem; From e6cf402f4a17f5e596f460c12549b95e60bab36d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Mar 2026 17:05:01 +0000 Subject: [PATCH 12/46] Rename Selection to Range --- client/src/services/context.ts | 77 +++++++++++++++----------------- client/src/services/events.ts | 18 ++++---- client/src/services/highlight.ts | 16 +++---- client/src/types/context.ts | 10 ++--- client/src/types/diagnostics.ts | 10 +---- client/src/webview/provider.ts | 2 +- client/src/webview/script.ts | 8 ++-- 7 files changed, 65 insertions(+), 76 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 247a693..5f50e1c 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -1,16 +1,16 @@ import { extension } from "../state"; -import { LJContext, Selection, LJVariable } from "../types/context"; +import { LJContext, Range, LJVariable } from "../types/context"; import { getOriginalVariableName } from "../utils/utils"; export function handleContext(context: LJContext) { extension.context = context; } -export function updateContextWithSelection(selection: Selection) { - const variablesInScope = getVariablesInScope(extension.file, selection) || []; +export function updateContext(range: Range) { + const variablesInScope = getVariablesInScope(extension.file, range) || []; const instanceVariables = filterInstanceVariables(extension.context.instanceVars || [], variablesInScope); const globalVariables = extension.context.globalVars || []; - const visibleInstanceVariables = getVisibleVariables(instanceVariables, extension.file, selection); + const visibleInstanceVariables = getVisibleVariables(instanceVariables, extension.file, range); const allVars = sortVariables(filterDuplicateVariables([...variablesInScope, ...globalVariables, ...visibleInstanceVariables])); extension.context.varsInScope = variablesInScope; extension.context.allVars = allVars; @@ -18,21 +18,21 @@ export function updateContextWithSelection(selection: Selection) { // 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): LJVariable[] | null { +export function getVariablesInScope(file: string, range: Range): LJVariable[] | null { // get variables in file const fileVars = extension.context.vars[file]; if (!fileVars) return null; - const normalizedSelection = normalizeSelection(selection); + const normalizedRange = normalizeRange(range); - // get variables in the current scope based on the selection + // get variables in the current scope based on the range let mostSpecificScope: string | null = null; let minScopeSize = Infinity; - // find the most specific scope that contains the selection + // find the most specific scope that contains the range for (const scope of Object.keys(fileVars)) { - const scopeSelection = parseScopeString(scope); - if (isSelectionWithinAnother(normalizedSelection, scopeSelection)) { - const scopeSize = (scopeSelection.endLine - scopeSelection.startLine) * 10000 + (scopeSelection.endColumn - scopeSelection.startColumn); + const scopeRange: Range = parseScopeString(scope); + if (isRangeWithin(normalizedRange, scopeRange)) { + const scopeSize = (scopeRange.lineEnd - scopeRange.lineStart) * 10000 + (scopeRange.colEnd - scopeRange.colStart); if (scopeSize < minScopeSize) { mostSpecificScope = scope; minScopeSize = scopeSize; @@ -44,66 +44,63 @@ export function getVariablesInScope(file: string, selection: Selection): LJVaria // filter variables to only include those that are reachable based on their position const variablesInScope = fileVars[mostSpecificScope]; - const reachableVariables = getVisibleVariables(variablesInScope, file, normalizedSelection); + const reachableVariables = getVisibleVariables(variablesInScope, file, normalizedRange); const visibleVariables = reachableVariables.filter(v => !v.name.includes("this#")); return visibleVariables; } -function getVisibleVariables(variables: LJVariable[], file: string, selection: Selection, useAnnotationPositions: boolean = false): LJVariable[] { - const isCollapsedSelection = - selection.startLine === selection.endLine && - selection.startColumn === selection.endColumn; - +function getVisibleVariables(variables: LJVariable[], file: string, range: Range, useAnnotationPositions: boolean = false): LJVariable[] { + const isCollapsedRange = range.lineStart === range.lineEnd && range.colStart === range.colEnd; return variables.filter((variable) => { if (variable.placementInCode?.position.file !== file) return false; // variable is not in the current file const placement = variable.placementInCode?.position; // single point cursor - if (isCollapsedSelection) { + if (isCollapsedRange) { const position = useAnnotationPositions ? variable.annPosition || placement : placement; - if (!position || 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) + if (!position || variable.isParameter) return true; // if is parameter we need to access it even if it's declared after the range (for method and parameter refinements) // variable was declared before the cursor line or its in the same line but before the cursor column return ( - position.line < selection.startLine || - (position.line === selection.startLine && position.column + 1 <= selection.startColumn) + position.line < range.lineStart || + (position.line === range.lineStart && position.column + 1 <= range.colStart) ); } - // range selection, filter variables that are only within the selection - const varSelection: Selection = { startLine: placement.line, startColumn: placement.column, endLine: placement.line, endColumn: placement.column } - return isSelectionWithinAnother(varSelection, selection); + // normal range, filter variables that are only within the range + const varRange: Range = { lineStart: placement.line, colStart: placement.column, lineEnd: placement.line, colEnd: placement.column } + return isRangeWithin(varRange, range); }); } -// Normalizes the selection to ensure start is before end -function normalizeSelection(selection: Selection): Selection { +// Normalizes the range to ensure start is before end +function normalizeRange(range: Range): Range { const startsBeforeEnds = - selection.startLine < selection.endLine || - (selection.startLine === selection.endLine && selection.startColumn <= selection.endColumn); + range.lineStart < range.lineEnd || + (range.lineStart === range.lineEnd && range.colStart <= range.colEnd); - if (startsBeforeEnds) return selection; + if (startsBeforeEnds) return range; return { - startLine: selection.endLine, - startColumn: selection.endColumn, - endLine: selection.startLine, - endColumn: selection.startColumn, + lineStart: range.lineEnd, + colStart: range.colEnd, + lineEnd: range.lineStart, + colEnd: range.colStart, }; } -function parseScopeString(scope: string): Selection { +function parseScopeString(scope: string): Range { const [start, end] = scope.split("-"); const [startLine, startColumn] = start.split(":").map(Number); const [endLine, endColumn] = end.split(":").map(Number); - return { startLine, startColumn, endLine, endColumn }; + return { lineStart: startLine, colStart: startColumn, lineEnd: endLine, colEnd: endColumn }; } -function isSelectionWithinAnother(selection: Selection, another: Selection): boolean { - const startsWithin = selection.startLine > another.startLine || - (selection.startLine === another.startLine && selection.startColumn >= another.startColumn); - const endsWithin = selection.endLine < another.endLine || - (selection.endLine === another.endLine && selection.endColumn <= another.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; } diff --git a/client/src/services/events.ts b/client/src/services/events.ts index feabb84..fbe8fb4 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -1,9 +1,9 @@ import * as vscode from 'vscode'; import { extension } from '../state'; import { updateStateMachine } from './state-machine'; -import { Selection } from '../types/context'; +import { Range } from '../types/context'; import { SELECTION_DEBOUNCE_MS } from '../utils/constants'; -import { updateContextWithSelection } from './context'; +import { updateContext } from './context'; let selectionTimeout: NodeJS.Timeout | null = null; @@ -59,14 +59,12 @@ export async function onSelectionChange(event: vscode.TextEditorSelectionChangeE */ function handleContextUpdate(selection: vscode.Selection) { if (!extension.file || !extension.context) return; - const selectionStart = selection.start; - const selectionEnd = selection.end; - const currentSelection: Selection = { - startLine: selectionStart.line, - startColumn: selectionStart.character, - endLine: selectionEnd.line, - endColumn: selectionEnd.character + const range: Range = { + lineStart: selection.start.line, + colStart: selection.start.character, + lineEnd: selection.end.line, + colEnd: selection.end.character }; - updateContextWithSelection(currentSelection); + updateContext(range); extension.webview?.sendMessage({ type: "context", context: extension.context }); } \ No newline at end of file diff --git a/client/src/services/highlight.ts b/client/src/services/highlight.ts index 990133c..37a6454 100644 --- a/client/src/services/highlight.ts +++ b/client/src/services/highlight.ts @@ -1,19 +1,19 @@ import * as vscode from 'vscode' -import { Selection } from '../types/context' +import { Range } from '../types/context' const highlight = vscode.window.createTextEditorDecorationType({ backgroundColor: 'rgba(255, 255, 0, 0.3)' }) -export function highlightRange(editor: vscode.TextEditor, selection: Selection) { - if (!selection) { +export function highlightRange(editor: vscode.TextEditor, range: Range) { + if (!range) { editor.setDecorations(highlight, []); return; } - const range = new vscode.Range( - new vscode.Position(selection.startLine, selection.startColumn), - new vscode.Position(selection.endLine, selection.endColumn) + const nativeRange = new vscode.Range( + new vscode.Position(range.lineStart, range.colStart), + new vscode.Position(range.lineEnd, range.colEnd) ) - editor.setDecorations(highlight, [{ range }]) - editor.revealRange(range, vscode.TextEditorRevealType.InCenter) + editor.setDecorations(highlight, [{ range: nativeRange }]) + editor.revealRange(nativeRange, vscode.TextEditorRevealType.InCenter) } \ No newline at end of file diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 401f913..f52e41b 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -39,9 +39,9 @@ export type LJContext = { allVars: LJVariable[]; // instance vars + global vars + vars in scope } -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..77ddcd8 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -1,14 +1,8 @@ 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; @@ -34,7 +28,7 @@ type BaseDiagnostic = { title: string; message: string; file: string; - position?: ErrorPosition; + position?: Range; } export type CustomError = BaseDiagnostic & { diff --git a/client/src/webview/provider.ts b/client/src/webview/provider.ts index 38a3179..9826815 100644 --- a/client/src/webview/provider.ts +++ b/client/src/webview/provider.ts @@ -45,7 +45,7 @@ export class LiquidJavaWebviewProvider implements vscode.WebviewViewProvider { }); } else if (message.type === "highlight") { // highlight the specified range in the current editor - highlightRange(vscode.window.activeTextEditor, message.selection); + highlightRange(vscode.window.activeTextEditor, message.range); } }); } diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index a1f7ff4..9a4b7ca 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -6,7 +6,7 @@ import type { LJDiagnostic } from "../types/diagnostics"; import type { LJStateMachine } from "../types/fsm"; import type { NavTab } from "./views/sections"; import { renderDiagnosticsView } from "./views/diagnostics/diagnostics"; -import { LJContext, Selection } from "../types/context"; +import { LJContext, Range } from "../types/context"; import { ContextSectionState, renderContextView } from "./views/context/context"; /** @@ -177,7 +177,7 @@ export function getScript(vscode: any, document: any, window: any) { previousSelected.classList.remove('selected'); if (previousSelected === target) { // remove highlight - vscode.postMessage({ type: 'highlight', selection: null }); + vscode.postMessage({ type: 'range', range: null }); return; } } @@ -188,8 +188,8 @@ export function getScript(vscode: any, document: any, window: any) { const endLine = parseInt(target.getAttribute('data-end-line') || '', 10); const endColumn = parseInt(target.getAttribute('data-end-column') || '', 10); if ([startLine, startColumn, endLine, endColumn].some(Number.isNaN)) return; - const selection: Selection = { startLine, startColumn, endLine, endColumn }; - vscode.postMessage({ type: 'highlight', selection }); + const range: Range = { lineStart: startLine, colStart: startColumn, lineEnd: endLine, colEnd: endColumn }; + vscode.postMessage({ type: 'range', range }); return; } From 0d5053db8d23ac24945a3ed4896622114d34fe3c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Mar 2026 17:57:24 +0000 Subject: [PATCH 13/46] Fix Positions --- client/src/services/context.ts | 19 +++++++++---------- client/src/services/events.ts | 2 +- client/src/services/highlight.ts | 2 +- client/src/services/webview.ts | 1 - client/src/types/context.ts | 4 ++-- client/src/types/diagnostics.ts | 8 ++++++-- client/src/webview/script.ts | 19 ++++++++++--------- client/src/webview/views/context/variables.ts | 11 +++++------ .../src/main/java/LJDiagnosticsHandler.java | 14 +++++++------- .../main/java/dtos/context/VariableDTO.java | 5 +++-- .../dtos/diagnostics/LJDiagnosticDTO.java | 5 ++--- .../dtos/diagnostics/SourcePositionDTO.java | 7 ++++--- .../java/dtos/diagnostics/SourceRangeDTO.java | 15 +++++++-------- .../java/dtos/warnings/CustomWarningDTO.java | 6 +++--- .../ExternalClassNotFoundWarningDTO.java | 6 +++--- .../ExternalMethodNotFoundWarningDTO.java | 6 +++--- .../main/java/dtos/warnings/LJWarningDTO.java | 6 +++--- 17 files changed, 69 insertions(+), 67 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 5f50e1c..2097f30 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -1,5 +1,6 @@ import { extension } from "../state"; import { LJContext, Range, LJVariable } from "../types/context"; +import { SourcePosition } from "../types/diagnostics"; import { getOriginalVariableName } from "../utils/utils"; export function handleContext(context: LJContext) { @@ -52,13 +53,12 @@ export function getVariablesInScope(file: string, range: Range): LJVariable[] | function getVisibleVariables(variables: LJVariable[], file: string, range: Range, useAnnotationPositions: boolean = false): LJVariable[] { const isCollapsedRange = range.lineStart === range.lineEnd && range.colStart === range.colEnd; return variables.filter((variable) => { - if (variable.placementInCode?.position.file !== file) return false; // variable is not in the current file - - const placement = variable.placementInCode?.position; + if (variable.position?.file !== file) return false; // variable is not in the current file // single point cursor if (isCollapsedRange) { - const position = useAnnotationPositions ? variable.annPosition || placement : placement; + const varPosition: SourcePosition = { line: variable.position.lineStart, column: variable.position.colStart, file }; + const position: SourcePosition = useAnnotationPositions ? variable.annPosition || varPosition : varPosition; if (!position || variable.isParameter) return true; // if is parameter we need to access it even if it's declared after the range (for method and parameter refinements) // variable was declared before the cursor line or its in the same line but before the cursor column @@ -68,8 +68,7 @@ function getVisibleVariables(variables: LJVariable[], file: string, range: Range ); } // normal range, filter variables that are only within the range - const varRange: Range = { lineStart: placement.line, colStart: placement.column, lineEnd: placement.line, colEnd: placement.column } - return isRangeWithin(varRange, range); + return isRangeWithin(variable.position, range); }); } @@ -117,16 +116,16 @@ function filterDuplicateVariables(variables: LJVariable[]): LJVariable[] { function sortVariables(variables: LJVariable[]): LJVariable[] { // sort by position or name return variables.sort((left, right) => { - const leftPosition = left.placementInCode?.position - const rightPosition = right.placementInCode?.position + const leftPosition = left.position + const rightPosition = right.position if (!leftPosition && !rightPosition) return compareVariableNames(left, right); if (!leftPosition) return 1; if (!rightPosition) return -1; if (getOriginalVariableName(left.name) === "ret") return 1; if (getOriginalVariableName(right.name) === "ret") return -1; - if (leftPosition.line !== rightPosition.line) return leftPosition.line - rightPosition.line; - if (leftPosition.column !== rightPosition.column) return leftPosition.column - rightPosition.column; + if (leftPosition.lineStart !== rightPosition.lineStart) return leftPosition.lineStart - rightPosition.lineStart; + if (leftPosition.colStart !== rightPosition.colStart) return leftPosition.colStart - rightPosition.colStart; return compareVariableNames(left, right); }); diff --git a/client/src/services/events.ts b/client/src/services/events.ts index fbe8fb4..84081b4 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -1,9 +1,9 @@ import * as vscode from 'vscode'; import { extension } from '../state'; import { updateStateMachine } from './state-machine'; -import { Range } from '../types/context'; import { SELECTION_DEBOUNCE_MS } from '../utils/constants'; import { updateContext } from './context'; +import { Range } from '../types/context'; let selectionTimeout: NodeJS.Timeout | null = null; diff --git a/client/src/services/highlight.ts b/client/src/services/highlight.ts index 37a6454..09fb6d1 100644 --- a/client/src/services/highlight.ts +++ b/client/src/services/highlight.ts @@ -1,5 +1,5 @@ import * as vscode from 'vscode' -import { Range } from '../types/context' +import { Range } from '../types/context'; const highlight = vscode.window.createTextEditorDecorationType({ backgroundColor: 'rgba(255, 255, 0, 0.3)' diff --git a/client/src/services/webview.ts b/client/src/services/webview.ts index e6a5f7d..e4d7dbe 100644 --- a/client/src/services/webview.ts +++ b/client/src/services/webview.ts @@ -22,7 +22,6 @@ 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") { if (extension.file) extension.webview.sendMessage({ type: "file", file: extension.file }); if (extension.diagnostics) extension.webview.sendMessage({ type: "diagnostics", diagnostics: extension.diagnostics }); diff --git a/client/src/types/context.ts b/client/src/types/context.ts index f52e41b..93e9506 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -1,4 +1,4 @@ -import { PlacementInCode, SourcePosition } from "./diagnostics"; +import { SourcePosition, SourceRange } from "./diagnostics"; // Type definitions used for LiquidJava context information @@ -7,7 +7,7 @@ export type LJVariable = { type: string; refinement: string; mainRefinement: string; - placementInCode: PlacementInCode | null; + position: SourceRange| null; isParameter: boolean; annPosition: SourcePosition | null; failingRefinement: string | null; diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 77ddcd8..2c64492 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -4,11 +4,15 @@ import type { Range } from './context'; // Type definitions used for LiquidJava diagnostics export type SourcePosition = { - file: string; + file: string | null; line: number; column: number; } +export type SourceRange = Range & { + file: string | null; +} + export type PlacementInCode = { text: string; position: SourcePosition; @@ -28,7 +32,7 @@ type BaseDiagnostic = { title: string; message: string; file: string; - position?: Range; + position: SourceRange | null; } export type CustomError = BaseDiagnostic & { diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 9a4b7ca..ed84931 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -3,10 +3,11 @@ import { renderLoading } from "./views/loading"; import { renderStateMachineView } from "./views/fsm/fsm"; import { createMermaidDiagram, renderMermaidDiagram, resetZoom, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram"; import type { LJDiagnostic } from "../types/diagnostics"; +import type { Range } from "../types/context"; import type { LJStateMachine } from "../types/fsm"; import type { NavTab } from "./views/sections"; import { renderDiagnosticsView } from "./views/diagnostics/diagnostics"; -import { LJContext, Range } from "../types/context"; +import { LJContext } from "../types/context"; import { ContextSectionState, renderContextView } from "./views/context/context"; /** @@ -177,19 +178,19 @@ export function getScript(vscode: any, document: any, window: any) { previousSelected.classList.remove('selected'); if (previousSelected === target) { // remove highlight - vscode.postMessage({ type: 'range', range: null }); + vscode.postMessage({ type: 'highlight', range: null }); return; } } target.classList.add('selected'); - const startLine = parseInt(target.getAttribute('data-start-line') || '', 10); - const startColumn = parseInt(target.getAttribute('data-start-column') || '', 10); - const endLine = parseInt(target.getAttribute('data-end-line') || '', 10); - const endColumn = parseInt(target.getAttribute('data-end-column') || '', 10); - if ([startLine, startColumn, endLine, endColumn].some(Number.isNaN)) return; - const range: Range = { lineStart: startLine, colStart: startColumn, lineEnd: endLine, colEnd: endColumn }; - vscode.postMessage({ type: 'range', range }); + 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 }; + vscode.postMessage({ type: 'highlight', range }); return; } diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 59052a7..38e978e 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -27,16 +27,15 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool function renderVariable(variable: LJVariable): string { const variableName = getOriginalVariableName(variable.name); const refinement = variable.refinement !== "true" ? variable.refinement.replace("==", "=") : variable.name - const position = variable.placementInCode.position; // TODO: handle cases where we don't really have the correct position for the variable + const offset = variable.position.lineStart === variable.position.lineEnd && variable.position.colStart === variable.position.colEnd ? variableName.length : 0; return /*html*/`
${variable.failingRefinement ? /*html*/`⊢ ${variable.failingRefinement}` : ''} diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java index 4b80432..92024a6 100644 --- a/server/src/main/java/LJDiagnosticsHandler.java +++ b/server/src/main/java/LJDiagnosticsHandler.java @@ -13,11 +13,11 @@ 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 { @@ -77,7 +77,7 @@ public static List getDiagnostics(List 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()) @@ -99,18 +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) + 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/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index dbecebd..3c9a5dc 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -2,6 +2,7 @@ import dtos.diagnostics.PlacementInCodeDTO; import dtos.diagnostics.SourcePositionDTO; +import dtos.diagnostics.SourceRangeDTO; import liquidjava.processor.context.RefinedVariable; /** @@ -12,7 +13,7 @@ public record VariableDTO( String type, String refinement, String mainRefinement, - PlacementInCodeDTO placementInCode, + SourceRangeDTO position, boolean isParameter, SourcePositionDTO annPosition, String failingRefinement @@ -23,7 +24,7 @@ public static VariableDTO from(RefinedVariable refinedVariable) { ContextHistoryDTO.stringifyType(refinedVariable.getType()), refinedVariable.getRefinement().toString(), refinedVariable.getMainRefinement().toString(), - PlacementInCodeDTO.from(refinedVariable.getPlacementInCode()), + SourceRangeDTO.from(refinedVariable.getPlacementInCode().getPosition()), refinedVariable.isParameter(), SourcePositionDTO.from(refinedVariable.getAnnPosition()), refinedVariable.getFailingRefinement() != null ? refinedVariable.getFailingRefinement().toString() : null 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..dea975d 100644 --- a/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java +++ b/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java @@ -7,8 +7,9 @@ */ public record SourcePositionDTO(String file, int line, int column) { - public static SourcePositionDTO from(SourcePosition position) { - String file = position.getFile() != null ? position.getFile().getAbsolutePath() : ""; - return new SourcePositionDTO(file, position.getLine() - 1, position.getColumn() - 1); + 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); } } diff --git a/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java b/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java index 6b25880..2586c23 100644 --- a/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java +++ b/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java @@ -1,14 +1,13 @@ package dtos.diagnostics; -import liquidjava.diagnostics.ErrorPosition; +import spoon.reflect.cu.SourcePosition; -public record SourceRangeDTO(int lineStart, int colStart, int lineEnd, int colEnd) { +public record SourceRangeDTO(String file, int lineStart, int colStart, int lineEnd, int colEnd) { - public static SourceRangeDTO from(ErrorPosition pos) { - if (pos == null) { - // no location information available - return new SourceRangeDTO(0, 0, 0, 0); - } - return new SourceRangeDTO(pos.lineStart() - 1, pos.colStart() - 1, pos.lineEnd() - 1, pos.colEnd() - 1); + public static SourceRangeDTO from(SourcePosition pos) { + if (pos == null) return null; + String file = pos.getFile() != null ? pos.getFile().getAbsolutePath() : null; + return new SourceRangeDTO(file, pos.getLine() - 1, pos.getColumn() - 1, pos.getEndLine() - 1, pos.getEndColumn() - 1); } } + diff --git a/server/src/main/java/dtos/warnings/CustomWarningDTO.java b/server/src/main/java/dtos/warnings/CustomWarningDTO.java index ccfebfc..dab3afb 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.SourceRangeDTO; 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, SourceRangeDTO position) { public static CustomWarningDTO from(CustomWarning warning) { return new CustomWarningDTO("warning", "custom-warning", warning.getTitle(), warning.getMessage(), warning.getFile(), - warning.getPosition()); + SourceRangeDTO.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..3f53a0c 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.SourceRangeDTO; 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) { + SourceRangeDTO 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()); + SourceRangeDTO.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..9ba0d6e 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.SourceRangeDTO; 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) { + SourceRangeDTO 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()); + SourceRangeDTO.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..88add1f 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.SourceRangeDTO; 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, SourceRangeDTO 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(), SourceRangeDTO.from(warning.getPosition())); } } From 04766b6de34688fe4e75a3a3c4acb85415d49291 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 6 Mar 2026 17:35:48 +0000 Subject: [PATCH 14/46] Fix Context Update --- client/src/lsp/client.ts | 2 +- client/src/services/context.ts | 3 +++ client/src/services/diagnostics.ts | 2 +- client/src/services/events.ts | 1 + client/src/state.ts | 3 ++- 5 files changed, 8 insertions(+), 3 deletions(-) diff --git a/client/src/lsp/client.ts b/client/src/lsp/client.ts index d01bdc0..4cadccc 100644 --- a/client/src/lsp/client.ts +++ b/client/src/lsp/client.ts @@ -45,7 +45,7 @@ export async function runClient(context: vscode.ExtensionContext, port: number) }); extension.client.onNotification("liquidjava/context", (context: LJContext) => { - handleContext({...context, varsInScope: [], allVars: []}); + handleContext(context); }); const editor = vscode.window.activeTextEditor; diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 2097f30..0d794e1 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -5,9 +5,12 @@ import { getOriginalVariableName } from "../utils/utils"; export function handleContext(context: LJContext) { extension.context = context; + updateContext(extension.currentSelection); + extension.webview.sendMessage({ type: "context", context: extension.context }); } export function updateContext(range: Range) { + if (!range) return; const variablesInScope = getVariablesInScope(extension.file, range) || []; const instanceVariables = filterInstanceVariables(extension.context.instanceVars || [], variablesInScope); const globalVariables = extension.context.globalVars || []; 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/events.ts b/client/src/services/events.ts index 84081b4..792f61b 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -65,6 +65,7 @@ function handleContextUpdate(selection: vscode.Selection) { lineEnd: selection.end.line, colEnd: selection.end.character }; + extension.currentSelection = range; updateContext(range); extension.webview?.sendMessage({ type: "context", context: extension.context }); } \ No newline at end of file diff --git a/client/src/state.ts b/client/src/state.ts index 4bb357a..6e1736c 100644 --- a/client/src/state.ts +++ b/client/src/state.ts @@ -6,7 +6,7 @@ import { LiquidJavaLogger } from "./services/logger"; import { LiquidJavaWebviewProvider } from "./webview/provider"; import type { LJDiagnostic } from "./types/diagnostics"; import type { LJStateMachine } from "./types/fsm"; -import { LJContext } from "./types/context"; +import { LJContext, Range } from "./types/context"; export class ExtensionState { // server/client state @@ -24,6 +24,7 @@ export class ExtensionState { diagnostics?: LJDiagnostic[]; stateMachine?: LJStateMachine; context?: LJContext; + currentSelection?: Range; } export const extension = new ExtensionState(); \ No newline at end of file From 8e4bd4071de703c078485397fc05c1e9e1f38771 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Mar 2026 13:44:42 +0000 Subject: [PATCH 15/46] Fix Selection --- client/src/services/autocomplete.ts | 6 ++-- client/src/services/context.ts | 28 +++++++++---------- client/src/services/events.ts | 7 +++-- client/src/webview/styles.ts | 2 +- client/src/webview/views/context/variables.ts | 4 +-- 5 files changed, 25 insertions(+), 22 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index e34c536..39f2bc3 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -3,6 +3,7 @@ import { extension } from "../state"; import type { LJVariable, LJContext, LJGhost, LJAlias } from "../types/context"; import { getSimpleName } from "../utils/utils"; import { LIQUIDJAVA_ANNOTATION_START, LJAnnotation } from "../utils/constants"; +import { filterInstanceVariables } from "./context"; type CompletionItemOptions = { name: string; @@ -50,10 +51,11 @@ function getContextCompletionItems(context: LJContext, file: string, annotation: return getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints); } return []; - } + } const inScope = extension.context.varsInScope !== null; + const varsInScope = filterInstanceVariables(context.varsInScope || []) const itemsHandlers: Record vscode.CompletionItem[]> = { - vars: () => getVariableCompletionItems(extension.context.varsInScope || []), + vars: () => getVariableCompletionItems(varsInScope), ghosts: () => getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints), aliases: () => getAliasCompletionItems(context.aliases, triggerParameterHints), keywords: () => getKeywordsCompletionItems(triggerParameterHints, inScope), diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 0d794e1..ea11f63 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -12,11 +12,10 @@ export function handleContext(context: LJContext) { export function updateContext(range: Range) { if (!range) return; const variablesInScope = getVariablesInScope(extension.file, range) || []; - const instanceVariables = filterInstanceVariables(extension.context.instanceVars || [], variablesInScope); const globalVariables = extension.context.globalVars || []; - const visibleInstanceVariables = getVisibleVariables(instanceVariables, extension.file, range); - const allVars = sortVariables(filterDuplicateVariables([...variablesInScope, ...globalVariables, ...visibleInstanceVariables])); - extension.context.varsInScope = variablesInScope; + const visibleVariables = getVisibleVariables(variablesInScope, extension.file, range); + const allVars = sortVariables(filterDuplicateVariables([...visibleVariables, ...globalVariables])); + extension.context.varsInScope = visibleVariables; extension.context.allVars = allVars; } @@ -26,7 +25,6 @@ export function getVariablesInScope(file: string, range: Range): LJVariable[] | // get variables in file const fileVars = extension.context.vars[file]; if (!fileVars) return null; - const normalizedRange = normalizeRange(range); // get variables in the current scope based on the range let mostSpecificScope: string | null = null; @@ -35,7 +33,7 @@ export function getVariablesInScope(file: string, range: Range): LJVariable[] | // find the most specific scope that contains the range for (const scope of Object.keys(fileVars)) { const scopeRange: Range = parseScopeString(scope); - if (isRangeWithin(normalizedRange, scopeRange)) { + if (isRangeWithin(range, scopeRange)) { const scopeSize = (scopeRange.lineEnd - scopeRange.lineStart) * 10000 + (scopeRange.colEnd - scopeRange.colStart); if (scopeSize < minScopeSize) { mostSpecificScope = scope; @@ -48,9 +46,8 @@ export function getVariablesInScope(file: string, range: Range): LJVariable[] | // filter variables to only include those that are reachable based on their position const variablesInScope = fileVars[mostSpecificScope]; - const reachableVariables = getVisibleVariables(variablesInScope, file, normalizedRange); - const visibleVariables = reachableVariables.filter(v => !v.name.includes("this#")); - return visibleVariables; + variablesInScope.push(...filterRelevantInstanceVariables(extension.context.instanceVars || [], variablesInScope)); + return getVisibleVariables(variablesInScope, file, range); } function getVisibleVariables(variables: LJVariable[], file: string, range: Range, useAnnotationPositions: boolean = false): LJVariable[] { @@ -76,13 +73,12 @@ function getVisibleVariables(variables: LJVariable[], file: string, range: Range } // Normalizes the range to ensure start is before end -function normalizeRange(range: Range): Range { - const startsBeforeEnds = +export function normalizeRange(range: Range): Range { + const isStartBeforeEnd = range.lineStart < range.lineEnd || (range.lineStart === range.lineEnd && range.colStart <= range.colEnd); - if (startsBeforeEnds) return range; - + if (isStartBeforeEnd) return range; return { lineStart: range.lineEnd, colStart: range.colEnd, @@ -138,6 +134,10 @@ function compareVariableNames(a: LJVariable, b: LJVariable): number { return getOriginalVariableName(a.name).localeCompare(getOriginalVariableName(b.name)); } -function filterInstanceVariables(instanceVars: LJVariable[], variablesInScope: LJVariable[]): LJVariable[] { +function filterRelevantInstanceVariables(instanceVars: LJVariable[], variablesInScope: LJVariable[]): LJVariable[] { return instanceVars.filter(v => variablesInScope.some(s => s.name === getOriginalVariableName(v.name))); +} + +export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { + return variables.filter(v => !v.name.includes("#")); } \ No newline at end of file diff --git a/client/src/services/events.ts b/client/src/services/events.ts index 792f61b..4597efc 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -2,7 +2,7 @@ import * as vscode from 'vscode'; import { extension } from '../state'; import { updateStateMachine } from './state-machine'; import { SELECTION_DEBOUNCE_MS } from '../utils/constants'; -import { updateContext } from './context'; +import { normalizeRange, updateContext } from './context'; import { Range } from '../types/context'; let selectionTimeout: NodeJS.Timeout | null = null; @@ -65,7 +65,8 @@ function handleContextUpdate(selection: vscode.Selection) { lineEnd: selection.end.line, colEnd: selection.end.character }; - extension.currentSelection = range; - updateContext(range); + const normalizedRange = normalizeRange(range); + extension.currentSelection = normalizedRange; + updateContext(normalizedRange); extension.webview?.sendMessage({ type: "context", context: extension.context }); } \ No newline at end of file diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index ba0b455..dbd618f 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -331,7 +331,7 @@ export function getStyles(): string { } .context-variable .failing-refinement { color: var(--vscode-editorError-foreground); - font-size: 0.9rem; + font-size: 0.8rem; } .diagram-section { margin-bottom: 1.5rem; diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 38e978e..3ada6d7 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -1,5 +1,5 @@ import { LJVariable } from "../../../types/context"; -import { getOriginalVariableName } from "../../utils"; +import { getOriginalVariableName, getSimpleName } from "../../utils"; import { renderToggleSection } from "../sections"; export function renderContextVariables(variables: LJVariable[], isExpanded: boolean): string { @@ -13,7 +13,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool ${variables.map(variable => /*html*/`
- + `).join('')} From 11dc8ac65e2191981634d9c5b18c45db36df4a54 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Mar 2026 13:47:15 +0000 Subject: [PATCH 16/46] Clear Highlight After Switching Tab --- client/src/webview/script.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index ed84931..4fc28c1 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -198,11 +198,11 @@ export function getScript(vscode: any, document: any, window: any) { if (target.classList.contains('nav-tab')) { e.stopPropagation(); const tab = target.getAttribute('data-tab') as NavTab; - console.log('Tab click:', tab); if (tab && tab !== selectedTab) { - console.log('Switching to tab:', tab); selectedTab = tab; updateView(); + if (selectedTab !== 'context') + vscode.postMessage({ type: 'highlight', range: null }); } return; } From 0a0e1472703572e8b6b98f0a3bba47c393964dc5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Mar 2026 14:31:54 +0000 Subject: [PATCH 17/46] Highlight Variables in TranslationTable --- client/src/services/autocomplete.ts | 4 +- client/src/services/context.ts | 13 +++--- client/src/types/context.ts | 6 +-- client/src/types/diagnostics.ts | 12 ++---- client/src/webview/script.ts | 4 +- client/src/webview/styles.ts | 6 +-- client/src/webview/views/context/variables.ts | 13 +----- .../views/diagnostics/derivation-nodes.ts | 4 +- client/src/webview/views/sections.ts | 41 ++++++++++++------- .../src/main/java/LJDiagnosticsHandler.java | 2 +- .../main/java/dtos/context/VariableDTO.java | 6 +-- .../dtos/diagnostics/SourcePositionDTO.java | 8 ++-- .../java/dtos/diagnostics/SourceRangeDTO.java | 13 ------ .../dtos/errors/ArgumentMismatchErrorDTO.java | 6 +-- .../main/java/dtos/errors/CustomErrorDTO.java | 6 +-- .../IllegalConstructorTransitionErrorDTO.java | 6 +-- .../errors/InvalidRefinementErrorDTO.java | 6 +-- .../src/main/java/dtos/errors/LJErrorDTO.java | 6 +-- .../java/dtos/errors/NotFoundErrorDTO.java | 6 +-- .../java/dtos/errors/RefinementErrorDTO.java | 6 +-- .../dtos/errors/StateConflictErrorDTO.java | 6 +-- .../dtos/errors/StateRefinementErrorDTO.java | 6 +-- .../main/java/dtos/errors/SyntaxErrorDTO.java | 6 +-- .../java/dtos/warnings/CustomWarningDTO.java | 6 +-- .../ExternalClassNotFoundWarningDTO.java | 6 +-- .../ExternalMethodNotFoundWarningDTO.java | 6 +-- .../main/java/dtos/warnings/LJWarningDTO.java | 6 +-- 27 files changed, 96 insertions(+), 120 deletions(-) delete mode 100644 server/src/main/java/dtos/diagnostics/SourceRangeDTO.java diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 39f2bc3..30b5de4 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -52,8 +52,8 @@ function getContextCompletionItems(context: LJContext, file: string, annotation: } return []; } - const inScope = extension.context.varsInScope !== null; - const varsInScope = filterInstanceVariables(context.varsInScope || []) + const inScope = extension.context.visibleVars !== null; + const varsInScope = filterInstanceVariables(context.visibleVars || []) const itemsHandlers: Record vscode.CompletionItem[]> = { vars: () => getVariableCompletionItems(varsInScope), ghosts: () => getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints), diff --git a/client/src/services/context.ts b/client/src/services/context.ts index ea11f63..9681256 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -13,10 +13,8 @@ export function updateContext(range: Range) { if (!range) return; const variablesInScope = getVariablesInScope(extension.file, range) || []; const globalVariables = extension.context.globalVars || []; - const visibleVariables = getVisibleVariables(variablesInScope, extension.file, range); - const allVars = sortVariables(filterDuplicateVariables([...visibleVariables, ...globalVariables])); - extension.context.varsInScope = visibleVariables; - extension.context.allVars = allVars; + extension.context.visibleVars = getVisibleVariables(variablesInScope, extension.file, range); + extension.context.allVars = sortVariables(filterDuplicateVariables([...extension.context.visibleVars, ...globalVariables])); } // Gets the variables in scope for a given file and position @@ -57,14 +55,13 @@ function getVisibleVariables(variables: LJVariable[], file: string, range: Range // single point cursor if (isCollapsedRange) { - const varPosition: SourcePosition = { line: variable.position.lineStart, column: variable.position.colStart, file }; - const position: SourcePosition = useAnnotationPositions ? variable.annPosition || varPosition : varPosition; + const position: SourcePosition = useAnnotationPositions ? variable.annPosition || variable.position : variable.position; if (!position || variable.isParameter) return true; // if is parameter we need to access it even if it's declared after the range (for method and parameter refinements) // variable was declared before the cursor line or its in the same line but before the cursor column return ( - position.line < range.lineStart || - (position.line === range.lineStart && position.column + 1 <= range.colStart) + position.lineStart < range.lineStart || + (position.lineStart === range.lineStart && position.colStart + 1 <= range.colStart) ); } // normal range, filter variables that are only within the range diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 93e9506..ffdf673 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -1,4 +1,4 @@ -import { SourcePosition, SourceRange } from "./diagnostics"; +import { SourcePosition } from "./diagnostics"; // Type definitions used for LiquidJava context information @@ -7,7 +7,7 @@ export type LJVariable = { type: string; refinement: string; mainRefinement: string; - position: SourceRange| null; + position: SourcePosition| null; isParameter: boolean; annPosition: SourcePosition | null; failingRefinement: string | null; @@ -35,7 +35,7 @@ export type LJContext = { instanceVars: LJVariable[]; globalVars: LJVariable[]; aliases: LJAlias[]; - varsInScope: LJVariable[]; // variables in scope for the current selection + visibleVars: LJVariable[]; // variables visible in the current selection allVars: LJVariable[]; // instance vars + global vars + vars in scope } diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts index 2c64492..16ba427 100644 --- a/client/src/types/diagnostics.ts +++ b/client/src/types/diagnostics.ts @@ -3,19 +3,13 @@ import type { Range } from './context'; // Type definitions used for LiquidJava diagnostics -export type SourcePosition = { - file: string | null; - line: number; - column: number; -} - -export type SourceRange = Range & { +export type SourcePosition = Range & { file: string | null; } export type PlacementInCode = { text: string; - position: SourcePosition; + position: SourcePosition | null; } export type TranslationTable = Record; @@ -32,7 +26,7 @@ type BaseDiagnostic = { title: string; message: string; file: string; - position: SourceRange | null; + position: SourcePosition | null; } export type CustomError = BaseDiagnostic & { diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 4fc28c1..f5e98d3 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -169,10 +169,10 @@ export function getScript(vscode: any, document: any, window: any) { } // highlight variable - if (target.classList.contains('context-variable-btn')) { + if (target.classList.contains('highlight-var-btn')) { e.stopPropagation(); - const previousSelected = root.querySelector('.context-variable-btn.selected'); + const previousSelected = root.querySelector('.highlight-var-btn.selected'); if (previousSelected) { // unselect previous previousSelected.classList.remove('selected'); diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index dbd618f..3aaeba5 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -318,15 +318,15 @@ export function getStyles(): string { .context-section-content.collapsed { display: none; } - .context-variable-btn { + .highlight-var-btn { background-color: transparent; border: none; transition: background-color 0.1s; } - .context-variable-btn code { + .highlight-var-btn code { pointer-events: none; } - .context-variable-btn.selected { + .highlight-var-btn.selected { background-color: var(--vscode-button-background); } .context-variable .failing-refinement { diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 3ada6d7..f0b7ef8 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -1,6 +1,6 @@ import { LJVariable } from "../../../types/context"; import { getOriginalVariableName, getSimpleName } from "../../utils"; -import { renderToggleSection } from "../sections"; +import { renderToggleSection, renderVariableHighlightButton } from "../sections"; export function renderContextVariables(variables: LJVariable[], isExpanded: boolean): string { return /*html*/` @@ -25,19 +25,10 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool } function renderVariable(variable: LJVariable): string { - const variableName = getOriginalVariableName(variable.name); const refinement = variable.refinement !== "true" ? variable.refinement.replace("==", "=") : variable.name - const offset = variable.position.lineStart === variable.position.lineEnd && variable.position.colStart === variable.position.colEnd ? variableName.length : 0; return /*html*/`
- + ${renderVariableHighlightButton(variable.position, refinement)} ${variable.failingRefinement ? /*html*/`⊢ ${variable.failingRefinement}` : ''}
`; } diff --git a/client/src/webview/views/diagnostics/derivation-nodes.ts b/client/src/webview/views/diagnostics/derivation-nodes.ts index 6c90a94..fcd6897 100644 --- a/client/src/webview/views/diagnostics/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 `${node.var}`; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 6687473..08df28e 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -1,4 +1,5 @@ -import type { LJDiagnostic, SourcePosition, TranslationTable } from "../../types/diagnostics"; +import type { LJDiagnostic, PlacementInCode, SourcePosition, TranslationTable } from "../../types/diagnostics"; +import { getOriginalVariableName } from "../utils"; export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
@@ -25,12 +26,7 @@ export const renderDiagnosticHeader = (diagnostic: LJDiagnostic): string => /*ht export const renderLocation = (diagnostic: LJDiagnostic): string => { if (!diagnostic.position || !diagnostic.file) return ""; - const position: SourcePosition = { - file: diagnostic.file, - line: diagnostic.position.lineStart, - column: diagnostic.position.colStart - } - return renderCustomSection("Location", /*html*/`
${renderLocationLink(position)}
`); + return renderCustomSection("Location", /*html*/`
${renderLocationLink(diagnostic.position)}
`); }; export function renderTranslationTable(translationTable: TranslationTable): string { @@ -44,17 +40,15 @@ export function renderTranslationTable(translationTable: TranslationTable): stri
- - ${entries.map(([variable, placement]: [string, any]) => { + ${entries.map(([variable, placement]: [string, PlacementInCode]) => { return /*html*/` - - + `; }).join('')} @@ -64,16 +58,33 @@ export function renderTranslationTable(translationTable: TranslationTable): stri `; } +export function renderVariableHighlightButton(position: SourcePosition, content: string): string { + return /*html*/` + + `; +} + export function renderLocationLink(position?: SourcePosition): string { if (!position) return 'No location'; - const file = `${position.file.split('/').pop().trim() || position.file}:${position.line + 1}`; return /*html*/`${file}`; + data-line="${position.lineStart}" + data-column="${position.colStart}" + >${getFile(position)}`; +} + +function getFile(position: SourcePosition): string { + return `${position.file.split('/').pop().trim() || position.file}:${position.lineStart + 1}`; } export type NavTab = 'diagnostics' | 'fsm' | 'context'; diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java index 92024a6..2028506 100644 --- a/server/src/main/java/LJDiagnosticsHandler.java +++ b/server/src/main/java/LJDiagnosticsHandler.java @@ -110,7 +110,7 @@ public static Range getRangeFromPosition(SourcePosition pos) { } return new Range( new Position(pos.getLine() - 1, pos.getColumn() - 1), - new Position(pos.getEndLine() - 1, pos.getEndColumn() - 1) + new Position(pos.getEndLine() - 1, pos.getEndColumn()) ); } } diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index 3c9a5dc..aeddf0d 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -1,8 +1,6 @@ package dtos.context; -import dtos.diagnostics.PlacementInCodeDTO; import dtos.diagnostics.SourcePositionDTO; -import dtos.diagnostics.SourceRangeDTO; import liquidjava.processor.context.RefinedVariable; /** @@ -13,7 +11,7 @@ public record VariableDTO( String type, String refinement, String mainRefinement, - SourceRangeDTO position, + SourcePositionDTO position, boolean isParameter, SourcePositionDTO annPosition, String failingRefinement @@ -24,7 +22,7 @@ public static VariableDTO from(RefinedVariable refinedVariable) { ContextHistoryDTO.stringifyType(refinedVariable.getType()), refinedVariable.getRefinement().toString(), refinedVariable.getMainRefinement().toString(), - SourceRangeDTO.from(refinedVariable.getPlacementInCode().getPosition()), + SourcePositionDTO.from(refinedVariable.getPlacementInCode().getPosition()), refinedVariable.isParameter(), SourcePositionDTO.from(refinedVariable.getAnnPosition()), refinedVariable.getFailingRefinement() != null ? refinedVariable.getFailingRefinement().toString() : null diff --git a/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java b/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java index dea975d..191c422 100644 --- a/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java +++ b/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java @@ -2,14 +2,12 @@ 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); + return new SourcePositionDTO(file, pos.getLine() - 1, pos.getColumn() - 1, pos.getEndLine() - 1, pos.getEndColumn()); } } + diff --git a/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java b/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java deleted file mode 100644 index 2586c23..0000000 --- a/server/src/main/java/dtos/diagnostics/SourceRangeDTO.java +++ /dev/null @@ -1,13 +0,0 @@ -package dtos.diagnostics; - -import spoon.reflect.cu.SourcePosition; - -public record SourceRangeDTO(String file, int lineStart, int colStart, int lineEnd, int colEnd) { - - public static SourceRangeDTO from(SourcePosition pos) { - if (pos == null) return null; - String file = pos.getFile() != null ? pos.getFile().getAbsolutePath() : null; - return new SourceRangeDTO(file, pos.getLine() - 1, pos.getColumn() - 1, pos.getEndLine() - 1, pos.getEndColumn() - 1); - } -} - diff --git a/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java b/server/src/main/java/dtos/errors/ArgumentMismatchErrorDTO.java index ebd16e5..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 dtos.diagnostics.SourceRangeDTO; +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, - SourceRangeDTO position) { + SourcePositionDTO position) { public static ArgumentMismatchErrorDTO from(ArgumentMismatchError error) { return new ArgumentMismatchErrorDTO("error", "argument-mismatch-error", error.getTitle(), error.getMessage(), error.getFile(), - SourceRangeDTO.from(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 510f481..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 dtos.diagnostics.SourceRangeDTO; +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, SourceRangeDTO 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(), - SourceRangeDTO.from(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 d65c195..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 dtos.diagnostics.SourceRangeDTO; +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, - SourceRangeDTO position) { + SourcePositionDTO position) { public static IllegalConstructorTransitionErrorDTO from(IllegalConstructorTransitionError error) { return new IllegalConstructorTransitionErrorDTO("error", "illegal-constructor-transition-error", error.getTitle(), error.getMessage(), error.getFile(), - SourceRangeDTO.from(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 0c4d465..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 dtos.diagnostics.SourceRangeDTO; +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, - SourceRangeDTO 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(), - SourceRangeDTO.from(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 8148da4..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.SourceRangeDTO; +import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.TranslationTableDTO; import liquidjava.diagnostics.errors.LJError; /** * DTO for serializing LJError instances to JSON */ -public record LJErrorDTO(String title, String message, String file, SourceRangeDTO 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(), - SourceRangeDTO.from(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 6fdce32..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.SourceRangeDTO; +import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.TranslationTableDTO; 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, SourceRangeDTO 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(), - SourceRangeDTO.from(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 641ed5f..18f1d7a 100644 --- a/server/src/main/java/dtos/errors/RefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/RefinementErrorDTO.java @@ -1,6 +1,6 @@ package dtos.errors; -import dtos.diagnostics.SourceRangeDTO; +import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.TranslationTableDTO; import liquidjava.diagnostics.errors.RefinementError; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; @@ -8,11 +8,11 @@ /** * DTO for serializing RefinementError instances to JSON */ -public record RefinementErrorDTO(String category, String type, String title, String message, String file, SourceRangeDTO 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(), - SourceRangeDTO.from(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 e81487e..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.SourceRangeDTO; +import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.TranslationTableDTO; 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, SourceRangeDTO 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(), - SourceRangeDTO.from(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 ca1a416..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.SourceRangeDTO; +import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.TranslationTableDTO; 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, SourceRangeDTO 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(), - SourceRangeDTO.from(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 c28d2cf..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 dtos.diagnostics.SourceRangeDTO; +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, SourceRangeDTO 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(), - SourceRangeDTO.from(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 dab3afb..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 dtos.diagnostics.SourceRangeDTO; +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, SourceRangeDTO 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(), - SourceRangeDTO.from(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 3f53a0c..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 dtos.diagnostics.SourceRangeDTO; +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, - SourceRangeDTO 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(), - SourceRangeDTO.from(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 9ba0d6e..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 dtos.diagnostics.SourceRangeDTO; +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, - SourceRangeDTO 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(), - SourceRangeDTO.from(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 88add1f..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 dtos.diagnostics.SourceRangeDTO; +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, SourceRangeDTO 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(), SourceRangeDTO.from(warning.getPosition())); + return new LJWarningDTO(warning.getTitle(), warning.getMessage(), warning.getFile(), SourcePositionDTO.from(warning.getPosition())); } } From 59b880f671cdbd58ece7947909372851c3e23fff Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Mar 2026 16:03:13 +0000 Subject: [PATCH 18/46] Fix Context Variables --- client/src/services/autocomplete.ts | 4 ++-- client/src/services/context.ts | 19 ++++++++++++++----- client/src/webview/views/context/variables.ts | 5 ++--- 3 files changed, 18 insertions(+), 10 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 30b5de4..a3822a2 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -3,7 +3,7 @@ import { extension } from "../state"; import type { LJVariable, LJContext, LJGhost, LJAlias } from "../types/context"; import { getSimpleName } from "../utils/utils"; import { LIQUIDJAVA_ANNOTATION_START, LJAnnotation } from "../utils/constants"; -import { filterInstanceVariables } from "./context"; +import { filterDuplicateVariables, filterInstanceVariables } from "./context"; type CompletionItemOptions = { name: string; @@ -53,7 +53,7 @@ function getContextCompletionItems(context: LJContext, file: string, annotation: return []; } const inScope = extension.context.visibleVars !== null; - const varsInScope = filterInstanceVariables(context.visibleVars || []) + const varsInScope = filterDuplicateVariables(filterInstanceVariables(context.visibleVars || [])); const itemsHandlers: Record vscode.CompletionItem[]> = { vars: () => getVariableCompletionItems(varsInScope), ghosts: () => getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints), diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 9681256..ca837ea 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -13,8 +13,10 @@ export function updateContext(range: Range) { if (!range) return; const variablesInScope = getVariablesInScope(extension.file, range) || []; const globalVariables = extension.context.globalVars || []; - extension.context.visibleVars = getVisibleVariables(variablesInScope, extension.file, range); - extension.context.allVars = sortVariables(filterDuplicateVariables([...extension.context.visibleVars, ...globalVariables])); + const visibleVars = getVisibleVariables(variablesInScope, extension.file, range); + const allVars = normalizeRefinements(sortVariables([...visibleVars, ...globalVariables])); + extension.context.visibleVars = visibleVars + extension.context.allVars = allVars; } // Gets the variables in scope for a given file and position @@ -43,8 +45,9 @@ export function getVariablesInScope(file: string, range: Range): LJVariable[] | return null; // filter variables to only include those that are reachable based on their position - const variablesInScope = fileVars[mostSpecificScope]; - variablesInScope.push(...filterRelevantInstanceVariables(extension.context.instanceVars || [], variablesInScope)); + const scopeVars = fileVars[mostSpecificScope]; + const instanceScopeVars = filterRelevantInstanceVariables(extension.context.instanceVars || [], scopeVars) + const variablesInScope = [...scopeVars, ...instanceScopeVars]; return getVisibleVariables(variablesInScope, file, range); } @@ -99,7 +102,7 @@ function isRangeWithin(range: Range, another: Range): boolean { return startsWithin && endsWithin; } -function filterDuplicateVariables(variables: LJVariable[]): LJVariable[] { +export function filterDuplicateVariables(variables: LJVariable[]): LJVariable[] { const uniqueVariables: Map = new Map(); for (const variable of variables) { if (!uniqueVariables.has(variable.name)) { @@ -137,4 +140,10 @@ function filterRelevantInstanceVariables(instanceVars: LJVariable[], variablesIn export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { return variables.filter(v => !v.name.includes("#")); +} + +function normalizeRefinements(variables: LJVariable[]): LJVariable[] { + return Array.from(new Map(variables.map(v => [v.refinement, v])).values()) // filter variables with duplicate refinements + .filter(v => !v.refinement.includes("==") || v.refinement.split("==").map(s => s.trim()).some((s, _, a) => s !== a[0])) // filter refinements that are just "var == var" + .map(v => ({ ...v, refinement: v.refinement.includes("==") ? v.refinement : `${v.name} == ${v.refinement}` })); // ensure refinements are in the form "var == refinement" } \ No newline at end of file diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index f0b7ef8..0e7b2c3 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -25,10 +25,9 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool } function renderVariable(variable: LJVariable): string { - const refinement = variable.refinement !== "true" ? variable.refinement.replace("==", "=") : variable.name return /*html*/`
- ${renderVariableHighlightButton(variable.position, refinement)} + ${renderVariableHighlightButton(variable.position, variable.refinement)} ${variable.failingRefinement ? /*html*/`⊢ ${variable.failingRefinement}` : ''}
`; -} +} \ No newline at end of file From 4cab61db5f703930cc371954c3e4d9e9d8414018 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Mar 2026 16:14:27 +0000 Subject: [PATCH 19/46] Improve `normalizeRefinements` --- client/src/services/context.ts | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index ca837ea..45fbf92 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -143,7 +143,12 @@ export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { } function normalizeRefinements(variables: LJVariable[]): LJVariable[] { - return Array.from(new Map(variables.map(v => [v.refinement, v])).values()) // filter variables with duplicate refinements - .filter(v => !v.refinement.includes("==") || v.refinement.split("==").map(s => s.trim()).some((s, _, a) => s !== a[0])) // filter refinements that are just "var == var" - .map(v => ({ ...v, refinement: v.refinement.includes("==") ? v.refinement : `${v.name} == ${v.refinement}` })); // ensure refinements are in the form "var == refinement" + return Array.from(new Map(variables.map(v => [v.refinement, v])).values()) // remove duplicates based on refinement + .flatMap(v => { + if (v.refinement.includes("==")) { + const [left, right] = v.refinement.split("==").map(s => s.trim()); + return left === right ? [] : [v]; // remove x == x refinements + } + return [{ ...v, refinement: `${v.name} == ${v.refinement}` }]; + }); } \ No newline at end of file From 3f4d6ec94ad0e3e5e043b7d1c74e7adea67fe2d6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Mar 2026 20:57:27 +0000 Subject: [PATCH 20/46] Get Failing Refinements By Diagnostic Position --- client/src/services/context.ts | 6 ++--- client/src/types/context.ts | 1 - client/src/webview/script.ts | 2 +- client/src/webview/styles.ts | 1 + client/src/webview/views/context/context.ts | 5 +++-- client/src/webview/views/context/variables.ts | 22 ++++++++++++++----- .../src/main/java/LJDiagnosticsHandler.java | 2 +- .../main/java/dtos/context/VariableDTO.java | 4 +--- 8 files changed, 27 insertions(+), 16 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 45fbf92..d6b567e 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -143,12 +143,12 @@ export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { } function normalizeRefinements(variables: LJVariable[]): LJVariable[] { - return Array.from(new Map(variables.map(v => [v.refinement, v])).values()) // remove duplicates based on refinement + return Array.from(new Map(variables.map(v => [v.refinement, v])).values()) .flatMap(v => { if (v.refinement.includes("==")) { const [left, right] = v.refinement.split("==").map(s => s.trim()); - return left === right ? [] : [v]; // remove x == x refinements + return left === right ? [] : [{ ...v, refinement: right }]; } - return [{ ...v, refinement: `${v.name} == ${v.refinement}` }]; + return v; }); } \ No newline at end of file diff --git a/client/src/types/context.ts b/client/src/types/context.ts index ffdf673..a67290c 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -10,7 +10,6 @@ export type LJVariable = { position: SourcePosition| null; isParameter: boolean; annPosition: SourcePosition | null; - failingRefinement: string | null; } export type LJGhost = { diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index f5e98d3..e39f447 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -246,7 +246,7 @@ export function getScript(vscode: any, document: any, window: any) { if (stateMachine) renderMermaidDiagram(document, window); break; case 'context': - root.innerHTML = renderContextView(context, currentFile, contextSectionState); + root.innerHTML = renderContextView(context, currentFile, contextSectionState, diagnostics); break; } } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 3aaeba5..09f29ac 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -322,6 +322,7 @@ export function getStyles(): string { background-color: transparent; border: none; transition: background-color 0.1s; + text-align: left; } .highlight-var-btn code { pointer-events: none; diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index fd328ba..4382e37 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -1,4 +1,5 @@ import { LJContext } from "../../../types/context"; +import { LJDiagnostic, SourcePosition } from "../../../types/diagnostics"; import { renderMainHeader } from "../sections"; import { renderContextAliases } from "./aliases"; import { renderContextGhosts } from "./ghosts"; @@ -10,7 +11,7 @@ export type ContextSectionState = { vars: boolean; } -export function renderContextView(context: LJContext, currentFile: string, sectionState: ContextSectionState): string { +export function renderContextView(context: LJContext, currentFile: string, sectionState: ContextSectionState, diagnostics: LJDiagnostic[]): string { if (!context || !currentFile) return ""; const allVars = context.allVars || []; @@ -24,7 +25,7 @@ export function renderContextView(context: LJContext, currentFile: string, secti ? '

No context information available for the current position.

' : `${renderContextAliases(aliases, sectionState.aliases)} ${renderContextGhosts(ghosts, sectionState.ghosts)} - ${renderContextVariables(allVars, sectionState.vars)} + ${renderContextVariables(allVars, sectionState.vars, diagnostics)} `} `; diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 0e7b2c3..0f6bb63 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -1,8 +1,9 @@ import { LJVariable } from "../../../types/context"; +import { LJDiagnostic, RefinementError, StateRefinementError } from "../../../types/diagnostics"; import { getOriginalVariableName, getSimpleName } from "../../utils"; import { renderToggleSection, renderVariableHighlightButton } from "../sections"; -export function renderContextVariables(variables: LJVariable[], isExpanded: boolean): string { +export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, diagnostics: LJDiagnostic[]): string { return /*html*/`
${renderToggleSection('Variables', 'context-vars', isExpanded)} @@ -12,7 +13,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool
${variables.map(variable => /*html*/` - + `).join('')} @@ -24,10 +25,21 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool `; } -function renderVariable(variable: LJVariable): string { +function renderVariable(variable: LJVariable, diagnostics: LJDiagnostic[]): string { + const failingRefinement = getFailingRefinement(variable, diagnostics); return /*html*/`
- ${renderVariableHighlightButton(variable.position, variable.refinement)} - ${variable.failingRefinement ? /*html*/`⊢ ${variable.failingRefinement}` : ''} + ${renderVariableHighlightButton(variable.position, `${variable.name} == ${variable.refinement}`)} + ${failingRefinement ? /*html*/`⊢ ${failingRefinement}` : ''}
`; +} + +function getFailingRefinement(variable: LJVariable, diagnostics: LJDiagnostic[]): string | null { + const matchingDiagnostic: RefinementError | StateRefinementError | undefined = diagnostics.find(d => + d.position && variable.position && + (d.type === 'refinement-error' || d.type === 'state-refinement-error') && + JSON.stringify(d.position) === JSON.stringify(variable.position) + ) as RefinementError | StateRefinementError | undefined; + return matchingDiagnostic ? matchingDiagnostic.type === 'refinement-error' ? + matchingDiagnostic.expected.value : matchingDiagnostic.expected : null; } \ No newline at end of file diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java index 2028506..92024a6 100644 --- a/server/src/main/java/LJDiagnosticsHandler.java +++ b/server/src/main/java/LJDiagnosticsHandler.java @@ -110,7 +110,7 @@ public static Range getRangeFromPosition(SourcePosition pos) { } return new Range( new Position(pos.getLine() - 1, pos.getColumn() - 1), - new Position(pos.getEndLine() - 1, pos.getEndColumn()) + new Position(pos.getEndLine() - 1, pos.getEndColumn() - 1) ); } } diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index aeddf0d..dddf795 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -14,7 +14,6 @@ public record VariableDTO( SourcePositionDTO position, boolean isParameter, SourcePositionDTO annPosition, - String failingRefinement ) { public static VariableDTO from(RefinedVariable refinedVariable) { return new VariableDTO( @@ -24,8 +23,7 @@ public static VariableDTO from(RefinedVariable refinedVariable) { refinedVariable.getMainRefinement().toString(), SourcePositionDTO.from(refinedVariable.getPlacementInCode().getPosition()), refinedVariable.isParameter(), - SourcePositionDTO.from(refinedVariable.getAnnPosition()), - refinedVariable.getFailingRefinement() != null ? refinedVariable.getFailingRefinement().toString() : null + SourcePositionDTO.from(refinedVariable.getAnnPosition()) ); } } \ No newline at end of file From e1fc9a4f6c1f0d71a042eeca312bf4ff5ffd85c9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 8 Mar 2026 19:28:26 +0000 Subject: [PATCH 21/46] Multiple Fixes --- client/src/services/context.ts | 16 +++++--------- client/src/webview/script.ts | 3 +-- client/src/webview/views/context/variables.ts | 22 +++++++++++++------ client/src/webview/views/sections.ts | 2 +- .../main/java/dtos/context/VariableDTO.java | 2 +- 5 files changed, 24 insertions(+), 21 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index d6b567e..52dac59 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -12,10 +12,11 @@ export function handleContext(context: LJContext) { export function updateContext(range: Range) { if (!range) return; const variablesInScope = getVariablesInScope(extension.file, range) || []; - const globalVariables = extension.context.globalVars || []; const visibleVars = getVisibleVariables(variablesInScope, extension.file, range); - const allVars = normalizeRefinements(sortVariables([...visibleVars, ...globalVariables])); - extension.context.visibleVars = visibleVars + const globalVariables = extension.context.globalVars || []; + console.log("global vars", globalVariables.length); + const allVars = sortVariables(normalizeRefinements([...globalVariables, ...visibleVars])); + extension.context.visibleVars = visibleVars; extension.context.allVars = allVars; } @@ -45,15 +46,14 @@ export function getVariablesInScope(file: string, range: Range): LJVariable[] | return null; // filter variables to only include those that are reachable based on their position - const scopeVars = fileVars[mostSpecificScope]; - const instanceScopeVars = filterRelevantInstanceVariables(extension.context.instanceVars || [], scopeVars) - const variablesInScope = [...scopeVars, ...instanceScopeVars]; + const variablesInScope = [...fileVars[mostSpecificScope], ...extension.context.instanceVars]; return getVisibleVariables(variablesInScope, file, range); } function getVisibleVariables(variables: LJVariable[], file: string, range: Range, useAnnotationPositions: boolean = false): LJVariable[] { const isCollapsedRange = range.lineStart === range.lineEnd && range.colStart === range.colEnd; 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 @@ -134,10 +134,6 @@ function compareVariableNames(a: LJVariable, b: LJVariable): number { return getOriginalVariableName(a.name).localeCompare(getOriginalVariableName(b.name)); } -function filterRelevantInstanceVariables(instanceVars: LJVariable[], variablesInScope: LJVariable[]): LJVariable[] { - return instanceVars.filter(v => variablesInScope.some(s => s.name === getOriginalVariableName(v.name))); -} - export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { return variables.filter(v => !v.name.includes("#")); } diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index e39f447..285b01f 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -199,10 +199,9 @@ export function getScript(vscode: any, document: any, window: any) { e.stopPropagation(); const tab = target.getAttribute('data-tab') as NavTab; if (tab && tab !== selectedTab) { + vscode.postMessage({ type: 'highlight', range: null }); selectedTab = tab; updateView(); - if (selectedTab !== 'context') - vscode.postMessage({ type: 'highlight', range: null }); } return; } diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 0f6bb63..6da9c65 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -35,11 +35,19 @@ function renderVariable(variable: LJVariable, diagnostics: LJDiagnostic[]): stri } function getFailingRefinement(variable: LJVariable, diagnostics: LJDiagnostic[]): string | null { - const matchingDiagnostic: RefinementError | StateRefinementError | undefined = diagnostics.find(d => - d.position && variable.position && - (d.type === 'refinement-error' || d.type === 'state-refinement-error') && - JSON.stringify(d.position) === JSON.stringify(variable.position) - ) as RefinementError | StateRefinementError | undefined; - return matchingDiagnostic ? matchingDiagnostic.type === 'refinement-error' ? - matchingDiagnostic.expected.value : matchingDiagnostic.expected : null; + // find refinement or state refinement error that matches the variable's position + const matchingDiagnostic = diagnostics.find((d): d is RefinementError | StateRefinementError => { + 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); + }); + if (!matchingDiagnostic) return null; + + // get the expected type from diagnostic + const expected = matchingDiagnostic.type === 'refinement-error' + ? matchingDiagnostic.expected.value + : matchingDiagnostic.expected; + + // only include those that mention the variable or "(this)" + return expected?.includes(variable.name) || expected?.includes('(this)') ? expected : null; } \ No newline at end of file diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 08df28e..3c3de0c 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -40,7 +40,7 @@ export function renderTranslationTable(translationTable: TranslationTable): stri - + diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index dddf795..0487632 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -13,7 +13,7 @@ public record VariableDTO( String mainRefinement, SourcePositionDTO position, boolean isParameter, - SourcePositionDTO annPosition, + SourcePositionDTO annPosition ) { public static VariableDTO from(RefinedVariable refinedVariable) { return new VariableDTO( From 288352d422c2d46d05e899ea9ab213ed828c1c05 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 8 Mar 2026 19:29:35 +0000 Subject: [PATCH 22/46] Cleanup --- client/src/services/context.ts | 1 - 1 file changed, 1 deletion(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 52dac59..285f894 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -14,7 +14,6 @@ export function updateContext(range: Range) { const variablesInScope = getVariablesInScope(extension.file, range) || []; const visibleVars = getVisibleVariables(variablesInScope, extension.file, range); const globalVariables = extension.context.globalVars || []; - console.log("global vars", globalVariables.length); const allVars = sortVariables(normalizeRefinements([...globalVariables, ...visibleVars])); extension.context.visibleVars = visibleVars; extension.context.allVars = allVars; From f4f32ab50490d17dcec3dab4505694ddbb43ab56 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 11:52:42 +0000 Subject: [PATCH 23/46] Use Ghosts as List --- client/src/services/autocomplete.ts | 5 +++-- client/src/types/context.ts | 3 ++- client/src/webview/views/context/context.ts | 6 +++--- .../main/java/dtos/context/ContextHistoryDTO.java | 2 +- server/src/main/java/dtos/context/GhostDTO.java | 6 ++++-- .../src/main/java/utils/ContextHistoryConverter.java | 12 +----------- 6 files changed, 14 insertions(+), 20 deletions(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index a3822a2..3c38492 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -46,9 +46,10 @@ export function registerAutocomplete(context: vscode.ExtensionContext) { 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 []; } @@ -56,7 +57,7 @@ function getContextCompletionItems(context: LJContext, file: string, annotation: const varsInScope = filterDuplicateVariables(filterInstanceVariables(context.visibleVars || [])); const itemsHandlers: Record vscode.CompletionItem[]> = { vars: () => getVariableCompletionItems(varsInScope), - ghosts: () => getGhostCompletionItems(context.ghosts[file] || [], triggerParameterHints), + ghosts: () => getGhostCompletionItems(ghosts, triggerParameterHints), aliases: () => getAliasCompletionItems(context.aliases, triggerParameterHints), keywords: () => getKeywordsCompletionItems(triggerParameterHints, inScope), types: () => getTypesCompletionItems(), diff --git a/client/src/types/context.ts b/client/src/types/context.ts index a67290c..713b2d4 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -19,6 +19,7 @@ export type LJGhost = { parameterTypes: string[]; refinement: string; isState: boolean; + file: string; } export type LJAlias = { @@ -30,9 +31,9 @@ export type LJAlias = { export type LJContext = { vars: Record>; // file -> (scope -> variables in scope) - ghosts: Record; // file -> ghosts in file instanceVars: LJVariable[]; globalVars: LJVariable[]; + ghosts: LJGhost[]; aliases: LJAlias[]; visibleVars: LJVariable[]; // variables visible in the current selection allVars: LJVariable[]; // instance vars + global vars + vars in scope diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index 4382e37..9730d2d 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -14,9 +14,9 @@ export type ContextSectionState = { export function renderContextView(context: LJContext, currentFile: string, sectionState: ContextSectionState, diagnostics: LJDiagnostic[]): string { if (!context || !currentFile) return ""; - const allVars = context.allVars || []; - const ghosts = context.ghosts[currentFile] || []; - const aliases = context.aliases || []; + 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*/`
diff --git a/server/src/main/java/dtos/context/ContextHistoryDTO.java b/server/src/main/java/dtos/context/ContextHistoryDTO.java index 2f3f86d..aa279e2 100644 --- a/server/src/main/java/dtos/context/ContextHistoryDTO.java +++ b/server/src/main/java/dtos/context/ContextHistoryDTO.java @@ -12,7 +12,7 @@ public record ContextHistoryDTO( Map>> vars, List instanceVars, List globalVars, - Map> ghosts, + List ghosts, List aliases ) { public static String stringifyType(CtTypeReference typeReference) { diff --git a/server/src/main/java/dtos/context/GhostDTO.java b/server/src/main/java/dtos/context/GhostDTO.java index e7521a4..825d796 100644 --- a/server/src/main/java/dtos/context/GhostDTO.java +++ b/server/src/main/java/dtos/context/GhostDTO.java @@ -15,7 +15,8 @@ public record GhostDTO( String returnType, List parameterTypes, String refinement, - boolean isState + boolean isState, + String file ) { private static final Pattern STATE_REFINEMENT_PATTERN = Pattern.compile("^state\\d+\\(_\\) == \\d+$"); @@ -29,7 +30,8 @@ public static GhostDTO from(GhostState ghostState) { ContextHistoryDTO.stringifyType(ghostState.getReturnType()), ghostState.getParametersTypes().stream().map(ContextHistoryDTO::stringifyType).collect(Collectors.toList()), refinement, - isState + isState, + ghostState.getFile() ); } } \ No newline at end of file diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index cfc19e2..3e98dda 100644 --- a/server/src/main/java/utils/ContextHistoryConverter.java +++ b/server/src/main/java/utils/ContextHistoryConverter.java @@ -11,7 +11,6 @@ import dtos.context.GhostDTO; import dtos.context.VariableDTO; import liquidjava.processor.context.ContextHistory; -import liquidjava.processor.context.GhostState; import liquidjava.processor.context.RefinedVariable; /** @@ -29,7 +28,7 @@ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) { 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.getGhosts().stream().map(GhostDTO::from).collect(Collectors.toList()), contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()) ); } @@ -47,13 +46,4 @@ private static Map>> toVariablesMap(Map> toGhostsMap(Map> ghosts) { - return ghosts.entrySet().stream().collect(Collectors.toMap( - Map.Entry::getKey, - entry -> entry.getValue().stream().map(GhostDTO::from).collect(Collectors.toList()), - (left, right) -> left, - HashMap::new - )); - } } From e6dcec7660c43d12a01c51679298c256a868f07e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 14:17:29 +0000 Subject: [PATCH 24/46] Add Hover for Failing Refinements --- client/src/webview/styles.ts | 28 +++++++++++++++++++ client/src/webview/utils.ts | 9 ++++++ client/src/webview/views/context/variables.ts | 20 ++++++------- 3 files changed, 46 insertions(+), 11 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 09f29ac..97ec539 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -333,6 +333,34 @@ export function getStyles(): string { .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; diff --git a/client/src/webview/utils.ts b/client/src/webview/utils.ts index 2e0fa36..f20bd89 100644 --- a/client/src/webview/utils.ts +++ b/client/src/webview/utils.ts @@ -6,4 +6,13 @@ export function getSimpleName(qualifiedName: string): string { export function getOriginalVariableName(name: string): string { return name.split("_")[0].replace(/^#/, ''); +} + +export function escapeHtml(html: string): string { + return html + .replace(/&/g, '&') + .replace(/"/g, '"') + .replace(/'/g, ''') + .replace(//g, '>'); } \ No newline at end of file diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 6da9c65..748c299 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -1,6 +1,6 @@ import { LJVariable } from "../../../types/context"; import { LJDiagnostic, RefinementError, StateRefinementError } from "../../../types/diagnostics"; -import { getOriginalVariableName, getSimpleName } from "../../utils"; +import { escapeHtml, getSimpleName } from "../../utils"; import { renderToggleSection, renderVariableHighlightButton } from "../sections"; export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, diagnostics: LJDiagnostic[]): string { @@ -26,28 +26,26 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool } function renderVariable(variable: LJVariable, diagnostics: LJDiagnostic[]): string { - const failingRefinement = getFailingRefinement(variable, diagnostics); + const diagnostic = getMatchingDiagnostic(variable, diagnostics); return /*html*/`
${renderVariableHighlightButton(variable.position, `${variable.name} == ${variable.refinement}`)} - ${failingRefinement ? /*html*/`⊢ ${failingRefinement}` : ''} + ${diagnostic ? /*html*/`⊢ ${diagnostic.expected}` : ''}
`; } -function getFailingRefinement(variable: LJVariable, diagnostics: LJDiagnostic[]): string | null { +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): d is RefinementError | StateRefinementError => { + 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; + const expected = matchingDiagnostic.type == "refinement-error" ? matchingDiagnostic.expected.value : matchingDiagnostic.expected; - // only include those that mention the variable or "(this)" - return expected?.includes(variable.name) || expected?.includes('(this)') ? expected : 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 From febce358f831422dc4b977d32c3bc03bd131b9f3 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 14:21:38 +0000 Subject: [PATCH 25/46] Minor Changes --- client/src/webview/views/context/aliases.ts | 2 +- client/src/webview/views/context/context.ts | 2 +- client/src/webview/views/context/ghosts.ts | 2 +- client/src/webview/views/context/variables.ts | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/client/src/webview/views/context/aliases.ts b/client/src/webview/views/context/aliases.ts index 45c6697..897c6d7 100644 --- a/client/src/webview/views/context/aliases.ts +++ b/client/src/webview/views/context/aliases.ts @@ -22,7 +22,7 @@ export function renderContextAliases(aliases: LJAlias[], isExpanded: boolean): s `).join('')}
VariableRefinementLocation
${variable.type} ${variable.name}${variable.refinement} - ${variable.placementInCode - ?`${renderLocationLink({ ...variable.placementInCode.position, column: variable.placementInCode.position.column + 1 })}` - : 'Unknown'} - ${renderVariable(variable)}${variable.type}
${renderVariable(variable)}${variable.type}${getSimpleName(variable.type)}
VariableSource Location
${variable}${placement.text}${renderLocationLink(placement.position)}${renderVariableHighlightButton(placement.position, placement.text)}
${renderVariable(variable)}${renderVariable(variable, diagnostics)} ${getSimpleName(variable.type)}
VariableLocationSource
- ` : '

No aliases available in the current file.

'} + ` : '

No aliases declared in the current project.

'}
`; diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index 9730d2d..d6aa743 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -22,7 +22,7 @@ export function renderContextView(context: LJContext, currentFile: string, secti
${renderMainHeader("", 'context')} ${total === 0 - ? '

No context information available for the current position.

' + ? '

No context information available.

' : `${renderContextAliases(aliases, sectionState.aliases)} ${renderContextGhosts(ghosts, sectionState.ghosts)} ${renderContextVariables(allVars, sectionState.vars, diagnostics)} diff --git a/client/src/webview/views/context/ghosts.ts b/client/src/webview/views/context/ghosts.ts index ab68371..3310935 100644 --- a/client/src/webview/views/context/ghosts.ts +++ b/client/src/webview/views/context/ghosts.ts @@ -18,7 +18,7 @@ export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): str `).join('')} - ` : '

No ghosts available in the current file.

'} + ` : '

No ghosts declared in the current file.

'}
`; diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 748c299..69af9f7 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -19,7 +19,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool `).join('')} - `: '

No variables available in the current position.

'} + `: '

No variables declared in the current position.

'}
`; From 385d32629013360eacb16fe8109f1dfefbdfc20b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 14:56:45 +0000 Subject: [PATCH 26/46] Remove Unused Imports --- client/src/webview/views/context/context.ts | 2 +- client/src/webview/views/fsm/fsm.ts | 2 +- client/src/webview/views/loading.ts | 2 +- client/src/webview/views/sections.ts | 1 - server/src/test/java/fsm/StateMachineParserTests.java | 1 - 5 files changed, 3 insertions(+), 5 deletions(-) diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index d6aa743..b43afde 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -1,5 +1,5 @@ import { LJContext } from "../../../types/context"; -import { LJDiagnostic, SourcePosition } from "../../../types/diagnostics"; +import { LJDiagnostic } from "../../../types/diagnostics"; import { renderMainHeader } from "../sections"; import { renderContextAliases } from "./aliases"; import { renderContextGhosts } from "./ghosts"; diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index e92bf77..593a162 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -1,5 +1,5 @@ import type { LJStateMachine } from "../../../types/fsm"; -import { renderMainHeader, type NavTab } from "../sections"; +import { renderMainHeader } from "../sections"; export function renderStateMachineView(sm: LJStateMachine, diagram: string, orientation: "LR" | "TB"): string { return /*html*/` 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*/`

LiquidJava

-

Starting verification...

+

Loading extension...

`; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 3c3de0c..b83ae00 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -1,5 +1,4 @@ import type { LJDiagnostic, PlacementInCode, SourcePosition, TranslationTable } from "../../types/diagnostics"; -import { getOriginalVariableName } from "../utils"; export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
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; From e583308bd7f64ce342ae1615b6b0ffa8b6f11401 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 15:08:02 +0000 Subject: [PATCH 27/46] Filter `true` Refinements --- client/src/services/context.ts | 1 + 1 file changed, 1 insertion(+) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 285f894..23fd00c 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -139,6 +139,7 @@ export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { function normalizeRefinements(variables: LJVariable[]): LJVariable[] { return Array.from(new Map(variables.map(v => [v.refinement, v])).values()) + .filter(v => v.refinement !== "true") .flatMap(v => { if (v.refinement.includes("==")) { const [left, right] = v.refinement.split("==").map(s => s.trim()); From d3d11ff197cc6ec6ad0f5c3e8673bab7541e8434 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 16:17:01 +0000 Subject: [PATCH 28/46] Use Scopes By File --- client/.vscode/launch.json | 3 - client/src/services/context.ts | 68 ++++++++----------- client/src/services/events.ts | 4 +- client/src/types/context.ts | 4 +- .../java/dtos/context/ContextHistoryDTO.java | 7 +- .../dtos/diagnostics/SourcePositionDTO.java | 17 ++++- .../java/utils/ContextHistoryConverter.java | 17 ++--- 7 files changed, 59 insertions(+), 61 deletions(-) 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/services/context.ts b/client/src/services/context.ts index 23fd00c..48d9d46 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -5,52 +5,49 @@ import { getOriginalVariableName } from "../utils/utils"; export function handleContext(context: LJContext) { extension.context = context; - updateContext(extension.currentSelection); + updateContextForSelection(extension.currentSelection); extension.webview.sendMessage({ type: "context", context: extension.context }); } -export function updateContext(range: Range) { - if (!range) return; - const variablesInScope = getVariablesInScope(extension.file, range) || []; - const visibleVars = getVisibleVariables(variablesInScope, extension.file, range); - const globalVariables = extension.context.globalVars || []; - const allVars = sortVariables(normalizeRefinements([...globalVariables, ...visibleVars])); +export function updateContextForSelection(selection: Range) { + if (!selection) return; + + const globalVars = extension.context.globalVars || []; + const localVars = extension.context.localVars || []; + const scope = getMostSpecificScope(extension.file, selection); + const variablesInScope = getVariablesInScope(localVars, extension.file, scope); + const visibleVars = getVisibleVariables(variablesInScope, extension.file, selection); + const allVars = sortVariables(normalizeRefinements([...globalVars, ...visibleVars])); extension.context.visibleVars = visibleVars; extension.context.allVars = allVars; } -// Gets the variables in scope for a given file and position -// Returns null if position not in any scope -export function getVariablesInScope(file: string, range: Range): LJVariable[] | null { - // get variables in file - const fileVars = extension.context.vars[file]; - if (!fileVars) return null; - - // get variables in the current scope based on the range - let mostSpecificScope: string | null = null; - let minScopeSize = Infinity; - +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 - for (const scope of Object.keys(fileVars)) { - const scopeRange: Range = parseScopeString(scope); - if (isRangeWithin(range, scopeRange)) { - const scopeSize = (scopeRange.lineEnd - scopeRange.lineStart) * 10000 + (scopeRange.colEnd - scopeRange.colStart); + 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; +} - // filter variables to only include those that are reachable based on their position - const variablesInScope = [...fileVars[mostSpecificScope], ...extension.context.instanceVars]; - return getVisibleVariables(variablesInScope, file, range); +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, range: Range, useAnnotationPositions: boolean = false): LJVariable[] { - const isCollapsedRange = range.lineStart === range.lineEnd && range.colStart === range.colEnd; +function getVisibleVariables(variables: LJVariable[], file: string, selection: Range, useAnnotationPositions: boolean = false): LJVariable[] { + const isCollapsedRange = selection.lineStart === selection.lineEnd && selection.colStart === selection.colEnd; 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 @@ -62,12 +59,12 @@ function getVisibleVariables(variables: LJVariable[], file: string, range: Range // variable was declared before the cursor line or its in the same line but before the cursor column return ( - position.lineStart < range.lineStart || - (position.lineStart === range.lineStart && position.colStart + 1 <= range.colStart) + position.lineStart < selection.lineStart || + (position.lineStart === selection.lineStart && position.colStart + 1 <= selection.colStart) ); } // normal range, filter variables that are only within the range - return isRangeWithin(variable.position, range); + return isRangeWithin(variable.position, selection); }); } @@ -86,13 +83,6 @@ export function normalizeRange(range: Range): Range { }; } -function parseScopeString(scope: string): Range { - const [start, end] = scope.split("-"); - const [startLine, startColumn] = start.split(":").map(Number); - const [endLine, endColumn] = end.split(":").map(Number); - return { lineStart: startLine, colStart: startColumn, lineEnd: endLine, colEnd: endColumn }; -} - function isRangeWithin(range: Range, another: Range): boolean { const startsWithin = range.lineStart > another.lineStart || (range.lineStart === another.lineStart && range.colStart >= another.colStart); diff --git a/client/src/services/events.ts b/client/src/services/events.ts index 4597efc..85bcc9d 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -2,7 +2,7 @@ import * as vscode from 'vscode'; import { extension } from '../state'; import { updateStateMachine } from './state-machine'; import { SELECTION_DEBOUNCE_MS } from '../utils/constants'; -import { normalizeRange, updateContext } from './context'; +import { normalizeRange, updateContextForSelection } from './context'; import { Range } from '../types/context'; let selectionTimeout: NodeJS.Timeout | null = null; @@ -67,6 +67,6 @@ function handleContextUpdate(selection: vscode.Selection) { }; const normalizedRange = normalizeRange(range); extension.currentSelection = normalizedRange; - updateContext(normalizedRange); + updateContextForSelection(normalizedRange); extension.webview?.sendMessage({ type: "context", context: extension.context }); } \ No newline at end of file diff --git a/client/src/types/context.ts b/client/src/types/context.ts index 713b2d4..e7ded81 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -30,13 +30,13 @@ export type LJAlias = { } export type LJContext = { - vars: Record>; // file -> (scope -> variables in scope) - instanceVars: LJVariable[]; + 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; // file -> scopes } export type Range = { diff --git a/server/src/main/java/dtos/context/ContextHistoryDTO.java b/server/src/main/java/dtos/context/ContextHistoryDTO.java index aa279e2..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>> vars, - List instanceVars, + List localVars, List globalVars, List ghosts, - List aliases + List aliases, + Map> fileScopes ) { public static String stringifyType(CtTypeReference typeReference) { if (typeReference == null) diff --git a/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java b/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java index 191c422..d00595e 100644 --- a/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java +++ b/server/src/main/java/dtos/diagnostics/SourcePositionDTO.java @@ -1,5 +1,8 @@ package dtos.diagnostics; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + import spoon.reflect.cu.SourcePosition; public record SourcePositionDTO(String file, int lineStart, int colStart, int lineEnd, int colEnd) { @@ -9,5 +12,17 @@ public static SourcePositionDTO from(SourcePosition pos) { 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; + + 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/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index 3e98dda..fb8b530 100644 --- a/server/src/main/java/utils/ContextHistoryConverter.java +++ b/server/src/main/java/utils/ContextHistoryConverter.java @@ -10,8 +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.RefinedVariable; /** * Utility class for converting LiquidJava context objects to DTOs. @@ -25,23 +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()), + parseFileScopes(contextHistory.getFileScopes()), + contextHistory.getLocalVars().stream().map(VariableDTO::from).collect(Collectors.toList()), contextHistory.getGlobalVars().stream().map(VariableDTO::from).collect(Collectors.toList()), contextHistory.getGhosts().stream().map(GhostDTO::from).collect(Collectors.toList()), contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()) ); } - private static Map>> toVariablesMap(Map>> vars) { - return vars.entrySet().stream().collect(Collectors.toMap( + private static Map> parseFileScopes(Map> 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 - )), + entry -> entry.getValue().stream().map(SourcePositionDTO::from).collect(Collectors.toList()), (left, right) -> left, HashMap::new )); From 2aafc2234c0e27a6b5ac91bdcd2b60e16cf9b01c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 16:27:14 +0000 Subject: [PATCH 29/46] Add Null Check --- client/src/services/context.ts | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 48d9d46..06d6bac 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -15,8 +15,13 @@ export function updateContextForSelection(selection: Range) { const globalVars = extension.context.globalVars || []; const localVars = extension.context.localVars || []; const scope = getMostSpecificScope(extension.file, selection); - const variablesInScope = getVariablesInScope(localVars, extension.file, scope); - const visibleVars = getVisibleVariables(variablesInScope, extension.file, selection); + + let visibleVars: LJVariable[] = []; + if (scope) { + const variablesInScope = getVariablesInScope(localVars, extension.file, scope); + visibleVars = getVisibleVariables(variablesInScope, extension.file, selection); + } + const allVars = sortVariables(normalizeRefinements([...globalVars, ...visibleVars])); extension.context.visibleVars = visibleVars; extension.context.allVars = allVars; From dc7fc8db809f906f5d275c89c95c3293b9a04429 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 16:46:29 +0000 Subject: [PATCH 30/46] Fix Highlighting Different File --- client/src/services/{highlight.ts => editor.ts} | 11 +++++++++++ client/src/webview/provider.ts | 13 ++----------- client/src/webview/script.ts | 8 +++++++- client/src/webview/views/sections.ts | 1 + .../main/java/utils/ContextHistoryConverter.java | 4 ++-- 5 files changed, 23 insertions(+), 14 deletions(-) rename client/src/services/{highlight.ts => editor.ts} (52%) diff --git a/client/src/services/highlight.ts b/client/src/services/editor.ts similarity index 52% rename from client/src/services/highlight.ts rename to client/src/services/editor.ts index 09fb6d1..2b33557 100644 --- a/client/src/services/highlight.ts +++ b/client/src/services/editor.ts @@ -5,6 +5,17 @@ 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, []); diff --git a/client/src/webview/provider.ts b/client/src/webview/provider.ts index 9826815..1cacfe9 100644 --- a/client/src/webview/provider.ts +++ b/client/src/webview/provider.ts @@ -1,6 +1,6 @@ import * as vscode from 'vscode'; import { getHtml } from './html'; -import { highlightRange } from '../services/highlight'; +import { highlightRange, openFile } from '../services/editor'; /** * Webview provider for the LiquidJava extension @@ -33,16 +33,7 @@ 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 position = new vscode.Position(message.line, message.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 285b01f..4bc34d8 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -184,13 +184,19 @@ export function getScript(vscode: any, document: any, window: any) { } 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 }; - vscode.postMessage({ type: 'highlight', range }); + if (file !== currentFile) { + vscode.postMessage({ type: 'openFile', filePath: file, line: lineStart, character: colStart, highlightRange: range }); + } else { + vscode.postMessage({ type: 'highlight', range }) + } return; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index b83ae00..6705edb 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -65,6 +65,7 @@ export function renderVariableHighlightButton(position: SourcePosition, content: data-start-column="${position.colStart}" data-end-line="${position.lineEnd}" data-end-column="${position.colEnd}" + data-file="${position.file}" > ${content} diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index fb8b530..748922a 100644 --- a/server/src/main/java/utils/ContextHistoryConverter.java +++ b/server/src/main/java/utils/ContextHistoryConverter.java @@ -25,11 +25,11 @@ public class ContextHistoryConverter { */ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) { return new ContextHistoryDTO( - parseFileScopes(contextHistory.getFileScopes()), contextHistory.getLocalVars().stream().map(VariableDTO::from).collect(Collectors.toList()), contextHistory.getGlobalVars().stream().map(VariableDTO::from).collect(Collectors.toList()), contextHistory.getGhosts().stream().map(GhostDTO::from).collect(Collectors.toList()), - contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()) + contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()), + parseFileScopes(contextHistory.getFileScopes()) ); } From 856625b0205a4b7adc80fd5d204dc51b4a748711 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 18:54:25 +0000 Subject: [PATCH 31/46] Minor Fix --- client/src/webview/styles.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 97ec539..0cf516e 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; From e4d07fec8bf4aac7422104bfcc75d2d48a3df74d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 19:10:35 +0000 Subject: [PATCH 32/46] Update Messages --- client/src/webview/views/context/aliases.ts | 2 +- client/src/webview/views/context/context.ts | 2 +- client/src/webview/views/context/ghosts.ts | 2 +- client/src/webview/views/context/variables.ts | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/client/src/webview/views/context/aliases.ts b/client/src/webview/views/context/aliases.ts index 897c6d7..6cd0f2f 100644 --- a/client/src/webview/views/context/aliases.ts +++ b/client/src/webview/views/context/aliases.ts @@ -22,7 +22,7 @@ export function renderContextAliases(aliases: LJAlias[], isExpanded: boolean): s `).join('')} - ` : '

No aliases declared in the current project.

'} + ` : '

No aliases declared in the project

'}
`; diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index b43afde..218a8be 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -22,7 +22,7 @@ export function renderContextView(context: LJContext, currentFile: string, secti
${renderMainHeader("", 'context')} ${total === 0 - ? '

No context information available.

' + ? '

No context information available at the cursor position

' : `${renderContextAliases(aliases, sectionState.aliases)} ${renderContextGhosts(ghosts, sectionState.ghosts)} ${renderContextVariables(allVars, sectionState.vars, diagnostics)} diff --git a/client/src/webview/views/context/ghosts.ts b/client/src/webview/views/context/ghosts.ts index 3310935..1a50b27 100644 --- a/client/src/webview/views/context/ghosts.ts +++ b/client/src/webview/views/context/ghosts.ts @@ -18,7 +18,7 @@ export function renderContextGhosts(ghosts: LJGhost[], isExpanded: boolean): str `).join('')} - ` : '

No ghosts declared in the current file.

'} + ` : '

No ghosts or states declared in the current file

'}
`; diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 69af9f7..53600ea 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -19,7 +19,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool `).join('')} - `: '

No variables declared in the current position.

'} + `: '

No variables declared at the cursor position

'} `; From 3762757a6acf91db5be20f6a29ceccd8d8f0708f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 19:15:40 +0000 Subject: [PATCH 33/46] Reverse Column Sort Order for Variables --- client/src/services/context.ts | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 06d6bac..37471d6 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -115,10 +115,8 @@ function sortVariables(variables: LJVariable[]): LJVariable[] { if (!leftPosition && !rightPosition) return compareVariableNames(left, right); if (!leftPosition) return 1; if (!rightPosition) return -1; - if (getOriginalVariableName(left.name) === "ret") return 1; - if (getOriginalVariableName(right.name) === "ret") return -1; if (leftPosition.lineStart !== rightPosition.lineStart) return leftPosition.lineStart - rightPosition.lineStart; - if (leftPosition.colStart !== rightPosition.colStart) return leftPosition.colStart - rightPosition.colStart; + if (leftPosition.colStart !== rightPosition.colStart) return rightPosition.colStart - leftPosition.colStart; return compareVariableNames(left, right); }); From 8cbee5ac63df2eefc01a4c90b1d44696d02d8fa4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 10 Mar 2026 13:37:24 +0000 Subject: [PATCH 34/46] Normalize Windows File Paths --- client/src/lsp/server.ts | 4 ++-- client/src/services/events.ts | 3 ++- client/src/utils/utils.ts | 5 +++++ 3 files changed, 9 insertions(+), 3 deletions(-) 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/events.ts b/client/src/services/events.ts index 85bcc9d..b471473 100644 --- a/client/src/services/events.ts +++ b/client/src/services/events.ts @@ -3,6 +3,7 @@ import { extension } from '../state'; import { updateStateMachine } from './state-machine'; 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; @@ -35,7 +36,7 @@ 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); diff --git a/client/src/utils/utils.ts b/client/src/utils/utils.ts index 305e775..14b233b 100644 --- a/client/src/utils/utils.ts +++ b/client/src/utils/utils.ts @@ -131,4 +131,9 @@ export function getSimpleName(qualifiedName: string): string { 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 From 072d2e53a317f211a6420ba95f98f7bae47629af Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 10 Mar 2026 14:36:54 +0000 Subject: [PATCH 35/46] Improve UI --- client/src/webview/styles.ts | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 0cf516e..d42f794 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -291,6 +291,21 @@ export function getStyles(): string { .context-section { margin-bottom: 1rem; } + .context-section table tr { + display: flex; + justify-content: space-between; + align-items: center; + } + .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; From 6c263790f10e76f46073fdbde0a175173d570117 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 10 Mar 2026 14:56:21 +0000 Subject: [PATCH 36/46] Fix View Updates --- client/src/webview/script.ts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 4bc34d8..1af0263 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -219,19 +219,19 @@ export function getScript(vscode: any, document: any, window: any) { switch (msg.type) { case 'diagnostics': diagnostics = msg.diagnostics as LJDiagnostic[]; - updateView(); + if (selectedTab === 'diagnostics') updateView(); break; case 'file': currentFile = msg.file; - if (!showAllDiagnostics) updateView(); + if (!showAllDiagnostics && selectedTab === 'diagnostics') updateView(); break; case 'fsm': stateMachine = msg.sm as LJStateMachine | undefined; - updateView(); + if (selectedTab === 'fsm') updateView(); break; case 'context': context = msg.context as LJContext; - updateView(); + if (selectedTab === 'context') updateView(); break; } }); From 10bfebb5b9e9170e319950303fcdfac77d39085c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 10 Mar 2026 23:37:56 +0000 Subject: [PATCH 37/46] Fix Variable Refinements --- client/src/services/context.ts | 13 +++++++++---- client/src/webview/views/context/variables.ts | 5 +++-- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 37471d6..3e08e8a 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -132,12 +132,17 @@ export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { function normalizeRefinements(variables: LJVariable[]): LJVariable[] { return Array.from(new Map(variables.map(v => [v.refinement, v])).values()) - .filter(v => v.refinement !== "true") - .flatMap(v => { + .filter(v => { + if (!v.refinement) return false; + if (v.refinement === "true") return false; // filter out trivial refinements if (v.refinement.includes("==")) { const [left, right] = v.refinement.split("==").map(s => s.trim()); - return left === right ? [] : [{ ...v, refinement: right }]; + return left !== right; // filter out tautologies like x == x } - return v; + return true; + }) + .flatMap(v => { + if (v.refinement.includes("==") || v.refinement.includes("!=")) return [v]; + return [{ ...v, refinement: `${v.name} == ${v.refinement}` }]; }); } \ No newline at end of file diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts index 53600ea..2536fa4 100644 --- a/client/src/webview/views/context/variables.ts +++ b/client/src/webview/views/context/variables.ts @@ -29,7 +29,7 @@ function renderVariable(variable: LJVariable, diagnostics: LJDiagnostic[]): stri const diagnostic = getMatchingDiagnostic(variable, diagnostics); return /*html*/`
- ${renderVariableHighlightButton(variable.position, `${variable.name} == ${variable.refinement}`)} + ${renderVariableHighlightButton(variable.position, variable.refinement)} ${diagnostic ? /*html*/`⊢ ${diagnostic.expected}` : ''}
`; } @@ -45,7 +45,8 @@ function getMatchingDiagnostic(variable: LJVariable, diagnostics: LJDiagnostic[] // 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; + return expected.includes(variable.name) ? { expected, message: `${matchingDiagnostic.title}: ${matchingDiagnostic.message}` } : null; } \ No newline at end of file From 8648b19510913d8a0d757b65822c045673ec2a21 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 10 Mar 2026 23:38:24 +0000 Subject: [PATCH 38/46] Fix Filter Instance Variables --- client/src/services/autocomplete.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/services/autocomplete.ts b/client/src/services/autocomplete.ts index 3c38492..8eb4b4d 100644 --- a/client/src/services/autocomplete.ts +++ b/client/src/services/autocomplete.ts @@ -54,7 +54,7 @@ function getContextCompletionItems(context: LJContext, file: string, annotation: return []; } const inScope = extension.context.visibleVars !== null; - const varsInScope = filterDuplicateVariables(filterInstanceVariables(context.visibleVars || [])); + const varsInScope = filterDuplicateVariables(filterInstanceVariables([...context.visibleVars || []])); const itemsHandlers: Record vscode.CompletionItem[]> = { vars: () => getVariableCompletionItems(varsInScope), ghosts: () => getGhostCompletionItems(ghosts, triggerParameterHints), From d3ca419cde01cf83ef109a5bad550e645b270846 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Mar 2026 00:10:56 +0000 Subject: [PATCH 39/46] Handle Variables with No Position --- server/src/main/java/dtos/context/VariableDTO.java | 5 ++++- server/src/main/java/utils/ContextHistoryConverter.java | 4 ++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index 0487632..cf09484 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -1,6 +1,7 @@ package dtos.context; import dtos.diagnostics.SourcePositionDTO; +import liquidjava.processor.context.PlacementInCode; import liquidjava.processor.context.RefinedVariable; /** @@ -16,12 +17,14 @@ public record VariableDTO( SourcePositionDTO annPosition ) { 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(), - SourcePositionDTO.from(refinedVariable.getPlacementInCode().getPosition()), + SourcePositionDTO.from(placement.getPosition()), refinedVariable.isParameter(), SourcePositionDTO.from(refinedVariable.getAnnPosition()) ); diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java index 748922a..10858fd 100644 --- a/server/src/main/java/utils/ContextHistoryConverter.java +++ b/server/src/main/java/utils/ContextHistoryConverter.java @@ -25,8 +25,8 @@ public class ContextHistoryConverter { */ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) { return new ContextHistoryDTO( - contextHistory.getLocalVars().stream().map(VariableDTO::from).collect(Collectors.toList()), - contextHistory.getGlobalVars().stream().map(VariableDTO::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()) From 091402c4cfd3b60268bb937a830ed897c65c1b0b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Mar 2026 00:14:32 +0000 Subject: [PATCH 40/46] Fix UI --- client/src/webview/styles.ts | 5 ----- 1 file changed, 5 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index d42f794..2e8a042 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -291,11 +291,6 @@ export function getStyles(): string { .context-section { margin-bottom: 1rem; } - .context-section table tr { - display: flex; - justify-content: space-between; - align-items: center; - } .context-section table td:first-child { text-align: left; flex: 1; From 00fe89295108308cbf76531d708ca4ec6f3c46a6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Mar 2026 11:52:59 +0000 Subject: [PATCH 41/46] Show All Refinements --- client/src/services/context.ts | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 3e08e8a..426d1d6 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -131,10 +131,9 @@ export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { } function normalizeRefinements(variables: LJVariable[]): LJVariable[] { - return Array.from(new Map(variables.map(v => [v.refinement, v])).values()) + return variables .filter(v => { if (!v.refinement) return false; - if (v.refinement === "true") return false; // filter out trivial refinements if (v.refinement.includes("==")) { const [left, right] = v.refinement.split("==").map(s => s.trim()); return left !== right; // filter out tautologies like x == x From 9f282788a8f2e217118cdb3ead984f7523eea709 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Mar 2026 14:13:52 +0000 Subject: [PATCH 42/46] Improve Refinement Normalization --- client/src/services/context.ts | 27 ++++++++++++--------------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 426d1d6..d36d525 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -22,7 +22,7 @@ export function updateContextForSelection(selection: Range) { visibleVars = getVisibleVariables(variablesInScope, extension.file, selection); } - const allVars = sortVariables(normalizeRefinements([...globalVars, ...visibleVars])); + const allVars = sortVariables(normalizeVariableRefinements([...globalVars, ...visibleVars])); extension.context.visibleVars = visibleVars; extension.context.allVars = allVars; } @@ -130,18 +130,15 @@ export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { return variables.filter(v => !v.name.includes("#")); } -function normalizeRefinements(variables: LJVariable[]): LJVariable[] { - return variables - .filter(v => { - if (!v.refinement) return false; - if (v.refinement.includes("==")) { - const [left, right] = v.refinement.split("==").map(s => s.trim()); - return left !== right; // filter out tautologies like x == x - } - return true; - }) - .flatMap(v => { - if (v.refinement.includes("==") || v.refinement.includes("!=")) return [v]; - return [{ ...v, refinement: `${v.name} == ${v.refinement}` }]; - }); +function normalizeVariableRefinements(variables: LJVariable[]): LJVariable[] { + return variables.flatMap(v => { + if (!v.refinement) return []; + if (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 From 7466d1528ccb61015da2854c33be7be4422f82a4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Mar 2026 14:52:27 +0000 Subject: [PATCH 43/46] Fix Variable Sorting --- client/src/services/context.ts | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index d36d525..faacb12 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -109,21 +109,20 @@ export function filterDuplicateVariables(variables: LJVariable[]): LJVariable[] function sortVariables(variables: LJVariable[]): LJVariable[] { // sort by position or name return variables.sort((left, right) => { - const leftPosition = left.position - const rightPosition = right.position - - if (!leftPosition && !rightPosition) return compareVariableNames(left, right); - if (!leftPosition) return 1; - if (!rightPosition) return -1; - if (leftPosition.lineStart !== rightPosition.lineStart) return leftPosition.lineStart - rightPosition.lineStart; - if (leftPosition.colStart !== rightPosition.colStart) return rightPosition.colStart - leftPosition.colStart; - + 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 { - return getOriginalVariableName(a.name).localeCompare(getOriginalVariableName(b.name)); + 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[] { From f7f4a739301ec5a1fdd4db62c39eb777cfa11d43 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Mar 2026 15:47:49 +0000 Subject: [PATCH 44/46] Filter Variables in Unreachable Scopes This fixes the issue where if a variable was declared in an unreachable scope it would still be shown in the context debugger and autocomplete. --- client/src/services/context.ts | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index faacb12..ab11e86 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -53,6 +53,7 @@ function getVariablesInScope(variables: LJVariable[], file: string, scope: Range function getVisibleVariables(variables: LJVariable[], file: string, selection: Range, useAnnotationPositions: boolean = false): 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 @@ -63,10 +64,16 @@ function getVisibleVariables(variables: LJVariable[], file: string, selection: R if (!position || variable.isParameter) return true; // if is parameter we need to access it even if it's declared after the range (for method and parameter refinements) // variable was declared before the cursor line or its in the same line but before the cursor column - return ( + const isDeclaredBeforeCursor = position.lineStart < selection.lineStart || - (position.lineStart === selection.lineStart && position.colStart + 1 <= selection.colStart) + (position.lineStart === selection.lineStart && position.colStart + 1 <= selection.colStart); + if (!isDeclaredBeforeCursor) return false; + + // 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); From 757b7ef9a485fac1444759d9cb6a4c711a994ba2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Mar 2026 19:05:51 +0000 Subject: [PATCH 45/46] Filter Duplicate Variable Refinements --- client/src/services/context.ts | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index ab11e86..9a35d87 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -137,9 +137,8 @@ export function filterInstanceVariables(variables: LJVariable[]): LJVariable[] { } function normalizeVariableRefinements(variables: LJVariable[]): LJVariable[] { - return variables.flatMap(v => { - if (!v.refinement) return []; - if (v.refinement === "true") return []; // filter out trivial refinements + 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 From a1919925d0d0f370f6c24eaf43cc4ff90566bfb4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 12 Mar 2026 15:59:26 +0000 Subject: [PATCH 46/46] Refactor Variable Positions --- client/src/services/context.ts | 6 +++--- client/src/types/context.ts | 3 +-- server/src/main/java/dtos/context/VariableDTO.java | 6 ++---- 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/client/src/services/context.ts b/client/src/services/context.ts index 9a35d87..47efe77 100644 --- a/client/src/services/context.ts +++ b/client/src/services/context.ts @@ -51,7 +51,7 @@ function getVariablesInScope(variables: LJVariable[], file: string, scope: Range return variables.filter(v => v.position?.file === file && isRangeWithin(v.position, scope)); } -function getVisibleVariables(variables: LJVariable[], file: string, selection: Range, useAnnotationPositions: boolean = false): LJVariable[] { +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) => { @@ -60,8 +60,8 @@ function getVisibleVariables(variables: LJVariable[], file: string, selection: R // single point cursor if (isCollapsedRange) { - const position: SourcePosition = useAnnotationPositions ? variable.annPosition || variable.position : variable.position; - if (!position || variable.isParameter) return true; // if is parameter we need to access it even if it's declared after the range (for method and parameter refinements) + 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 = diff --git a/client/src/types/context.ts b/client/src/types/context.ts index e7ded81..7943c9e 100644 --- a/client/src/types/context.ts +++ b/client/src/types/context.ts @@ -8,8 +8,7 @@ export type LJVariable = { refinement: string; mainRefinement: string; position: SourcePosition| null; - isParameter: boolean; - annPosition: SourcePosition | null; + annotationPosition: SourcePosition | null; } export type LJGhost = { diff --git a/server/src/main/java/dtos/context/VariableDTO.java b/server/src/main/java/dtos/context/VariableDTO.java index cf09484..60cada2 100644 --- a/server/src/main/java/dtos/context/VariableDTO.java +++ b/server/src/main/java/dtos/context/VariableDTO.java @@ -13,8 +13,7 @@ public record VariableDTO( String refinement, String mainRefinement, SourcePositionDTO position, - boolean isParameter, - SourcePositionDTO annPosition + SourcePositionDTO annotationPosition ) { public static VariableDTO from(RefinedVariable refinedVariable) { PlacementInCode placement = refinedVariable.getPlacementInCode(); @@ -25,8 +24,7 @@ public static VariableDTO from(RefinedVariable refinedVariable) { refinedVariable.getRefinement().toString(), refinedVariable.getMainRefinement().toString(), SourcePositionDTO.from(placement.getPosition()), - refinedVariable.isParameter(), - SourcePositionDTO.from(refinedVariable.getAnnPosition()) + SourcePositionDTO.from(placement.getAnnotationPosition()) ); } } \ No newline at end of file