Parallelize Verification and FSM

client/src/webview/views/context/context.ts

@@ -14,9 +14,9 @@ export type ContextSectionState = {
 export function renderContextView(context: LJContext, currentFile: string, sectionState: ContextSectionState, errorAtCursor?: RefinementMismatchError): string {
     if (!context || !currentFile) return "";
 
-    const allVars = context.allVars;
-    const ghosts = context.ghosts.filter(ghost => ghost.file === 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*/`
         <div>

server/src/main/java/LJDiagnosticsService.java

@@ -1,6 +1,9 @@
 import java.io.File;
 import java.net.URI;
 import java.util.List;
+import java.util.concurrent.CompletableFuture;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
@@ -24,6 +27,11 @@ public class LJDiagnosticsService implements TextDocumentService, WorkspaceServi
 
     private LJLanguageClient client;
     private String workspaceRoot;
+    private final ExecutorService diagnosticsExecutor = Executors.newSingleThreadExecutor(r -> {
+        Thread thread = new Thread(r, "liquidjava-diagnostics");
+        thread.setDaemon(true);
+        return thread;
+    });
 
     public void setClient(LJLanguageClient client) {
         this.client = client;
@@ -63,6 +71,22 @@ public void generateDiagnostics(String uri) {
         this.client.sendContext(ContextHistoryConverter.convertToDTO(ContextHistory.getInstance()));
     }
 
+    /**
+     * Schedules diagnostics generation without blocking the LSP thread
+     * @param uri the URI of the document
+     * @return a future that completes when diagnostics are published
+     */
+    public CompletableFuture<Void> generateDiagnosticsAsync(String uri) {
+        return CompletableFuture.runAsync(() -> generateDiagnostics(uri), diagnosticsExecutor);
+    }
+
+    /**
+     * Stops background diagnostics work
+     */
+    public void shutdown() {
+        diagnosticsExecutor.shutdownNow();
+    }
+
     /**
      * Clear a diagnostic for a specific URI
      * @param uri the URI of the document
@@ -82,7 +106,7 @@ public void didOpen(DidOpenTextDocumentParams params) {
         String uri = params.getTextDocument().getUri();
         if (!PathUtils.isFileInDirectory(uri, workspaceRoot)) return;
         System.out.println("Document opened — checking diagnostics");
-        generateDiagnostics(uri);
+        generateDiagnosticsAsync(uri);
     }
 
     /**
@@ -95,7 +119,7 @@ public void didSave(DidSaveTextDocumentParams params) {
         if (!PathUtils.isFileInDirectory(uri, workspaceRoot)) return;
         System.out.println("Document saved — checking diagnostics");
         clearDiagnostic(uri);
-        generateDiagnostics(uri);
+        generateDiagnosticsAsync(uri);
     }
 
     /**
@@ -130,4 +154,4 @@ public void didChangeConfiguration(DidChangeConfigurationParams params) {
     public void didChangeWatchedFiles(DidChangeWatchedFilesParams params) {
         // do nothing, ignore
     }
-}
+}

server/src/main/java/LJLanguageServer.java

@@ -1,4 +1,6 @@
 import java.util.concurrent.CompletableFuture;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
 
 import org.eclipse.lsp4j.InitializeParams;
 import org.eclipse.lsp4j.InitializeResult;
@@ -19,9 +21,15 @@
 public class LJLanguageServer implements LanguageServer {
 
     private final LJDiagnosticsService diagnosticsService;
+    private final ExecutorService stateMachineExecutor;
 
     public LJLanguageServer() {
         this.diagnosticsService = new LJDiagnosticsService();
+        this.stateMachineExecutor = Executors.newSingleThreadExecutor(r -> {
+            Thread thread = new Thread(r, "liquidjava-fsm");
+            thread.setDaemon(true);
+            return thread;
+        });
     }
 
     /**
@@ -57,6 +65,8 @@ public CompletableFuture<InitializeResult> initialize(InitializeParams params) {
     }
 
     public CompletableFuture<Object> shutdown() {
+        diagnosticsService.shutdown();
+        stateMachineExecutor.shutdownNow();
         return CompletableFuture.completedFuture(null);
     }
 
@@ -84,13 +94,11 @@ public void setTrace(Object params) {
 
     @JsonRequest("liquidjava/fsm")
     public CompletableFuture<StateMachine> fsm(Uri uri) {
-        return CompletableFuture.supplyAsync(() -> {
-            return StateMachineParser.parse(uri.uri());
-        });
+        return CompletableFuture.supplyAsync(() -> StateMachineParser.parse(uri.uri()), stateMachineExecutor);
     }
 
     @JsonNotification("liquidjava/verify")
     public void verify(Uri uri) {
-        diagnosticsService.generateDiagnostics(uri.uri());
+        diagnosticsService.generateDiagnosticsAsync(uri.uri());
     }
 }