Add Hover Navigation to Method Refinements

client/src/services/hover.ts

@@ -19,7 +19,11 @@ export function registerHover() {
                 hoverContent.appendCodeblock(formatRefinement(variable.mainRefinement), 'java');
             else {
                 const method = await getHoveredMethod(document, position);
-                if (method) hoverContent.appendCodeblock(formatMethodHover(method), 'java');
+                if (method) {
+                    hoverContent.appendCodeblock(formatMethodHover(method), 'java');
+                    const link = formatMethodLocationLink(method);
+                    if (link) hoverContent.appendMarkdown(`\n\n${link}`);
+                }
             }
 
             const diagnostics = vscode.languages.getDiagnostics(document.uri);
@@ -113,3 +117,11 @@ function formatMethodHover(method: LJMethod): string {
             .map(s => formatStateRefinement(s.from, s.to))
     ].filter(Boolean).join('\n');
 }
+
+function formatMethodLocationLink(method: LJMethod): string | null {
+    if (!method.position?.file) return null;
+    const uri = vscode.Uri.file(method.position.file).with({
+        fragment: `L${method.position.lineStart + 1},${method.position.colStart + 1}`
+    });
+    return `[Show Refinements](${uri.toString()})`;
+}

client/src/types/context.ts

@@ -40,6 +40,7 @@ export type LJMethod = {
   returnRefinement: string;
   parameters: LJVariable[];
   stateRefinements: LJMethodStateRefinement[];
+  position: SourcePosition | null;
 }
 
 export type LJContext = {

server/src/main/java/LJDiagnosticsHandler.java

@@ -23,8 +23,6 @@
 public class LJDiagnosticsHandler {
 
     private static final String SOURCE = "liquidjava";
-    private static final String LSP_FLAG = "-lsp";
-
     /**
      * Generates LJDiagnostics for the given URI
      * @param uri the document URI
@@ -35,7 +33,8 @@ public static LJDiagnostics getLJDiagnostics(String path) {
         List<LJError> errors = new ArrayList<>();
         List<LJWarning> warnings = new ArrayList<>();
         try {
-            CommandLineLauncher.main(new String[] { LSP_FLAG, path });
+            CommandLineLauncher.cmdArgs.lspMode = true;
+            CommandLineLauncher.launch(path);
             Diagnostics diagnostics = Diagnostics.getInstance();
             if (diagnostics.foundWarning()) {
                 warnings.addAll(diagnostics.getWarnings());

server/src/main/java/dtos/context/MethodDTO.java

@@ -3,6 +3,7 @@
 import java.util.List;
 import java.util.stream.Collectors;
 
+import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.processor.context.ObjectState;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.rj_language.Predicate;
@@ -16,15 +17,17 @@ public record MethodDTO(
     String targetClass,
     String returnRefinement,
     List<VariableDTO> parameters,
-    List<StateRefinementDTO> stateRefinements
+    List<StateRefinementDTO> stateRefinements,
+    SourcePositionDTO position
 ) {
     public static MethodDTO from(RefinedFunction refinedFunction) {
         return new MethodDTO(
             refinedFunction.getName(),
             refinedFunction.getTargetClass(),
             format(refinedFunction.getRefReturn()),
             refinedFunction.getArguments().stream().map(VariableDTO::from).filter(v -> v != null).collect(Collectors.toList()),
-            refinedFunction.getAllStates().stream().map(StateRefinementDTO::from).collect(Collectors.toList())
+            refinedFunction.getAllStates().stream().map(StateRefinementDTO::from).collect(Collectors.toList()),
+            SourcePositionDTO.from(refinedFunction.getPlacementInCode().getPosition())
         );
     }