Fix automatic restart of language server upon changes in configuration

eslint.config.mjs

@@ -24,7 +24,6 @@ export default tseslint.config(
       "@typescript-eslint/no-unsafe-member-access": "warn",
       "@typescript-eslint/dot-notation": "warn",
       "@typescript-eslint/no-explicit-any": "warn",
-      "@typescript-eslint/no-floating-promises": "warn"
     }
   },
   {

package.json

@@ -10,7 +10,7 @@
     "theme": "dark"
   },
   "license": "MIT",
-  "version": "0.0.39",
+  "version": "0.0.40",
   "repository": {
     "type": "git",
     "url": "https://github.com/imandra-ai/imandrax-vscode"

src/commands/implementations.ts

@@ -118,13 +118,13 @@ ${body}
   panel.webview.html = html;
 }
 
-export function checkAll(getClient: () => LanguageClient) {
+export async function checkAll(getClient: () => LanguageClient) {
   if (!getClient()) {
     return undefined;
   }
   const file_uri = window.activeTextEditor?.document.uri;
   if (getClient() && getClient().isRunning() && file_uri?.scheme === "file") {
-    getClient().sendRequest("workspace/executeCommand", { "command": "check-all", "arguments": [file_uri.toString()] });
+    await getClient().sendRequest("workspace/executeCommand", { "command": "check-all", "arguments": [file_uri.toString()] });
   }
 }
 
@@ -157,9 +157,9 @@ export function terminal_eval_selection(): boolean {
   return true;
 }
 
-export function clear_cache(getClient: () => LanguageClient) {
+export async function clear_cache(getClient: () => LanguageClient) {
   if (getClient()?.isRunning()) {
-    getClient().sendRequest("workspace/executeCommand", { "command": "clear-cache", "arguments": [] });
+    await getClient().sendRequest("workspace/executeCommand", { "command": "clear-cache", "arguments": [] });
   }
   return true;
 }

src/commands/registration.ts

@@ -1,19 +1,19 @@
 import * as implementations from './implementations';
 
 import { commands, ExtensionContext, languages, Uri, ViewColumn, window, workspace } from 'vscode';
-import { ImandraxLanguageClient } from '../imandrax_language_client/imandrax_language_client';
+import { ImandraXLanguageClient } from '../imandrax_language_client/imandrax_language_client';
 
-export function register(context: ExtensionContext, imandraxLanguageClient: ImandraxLanguageClient) {
+export function register(context: ExtensionContext, imandraxLanguageClient: ImandraXLanguageClient) {
   const getClient = () => { return imandraxLanguageClient.getClient(); };
 
   const restart_cmd = "imandrax.restart_language_server";
-  const restart_handler = () => {
-    imandraxLanguageClient.restart({ extensionUri: context.extensionUri });
+  const restart_handler = async () => {
+    await imandraxLanguageClient.restart({ extensionUri: context.extensionUri });
   };
   context.subscriptions.push(commands.registerCommand(restart_cmd, restart_handler));
 
   const check_all_cmd = "imandrax.check_all";
-  const check_all_handler = () => { implementations.checkAll(getClient); };
+  const check_all_handler = async () => { await implementations.checkAll(getClient); };
   context.subscriptions.push(commands.registerCommand(check_all_cmd, check_all_handler));
 
   const browse_cmd = "imandrax.browse";
@@ -33,7 +33,7 @@ export function register(context: ExtensionContext, imandraxLanguageClient: Iman
   context.subscriptions.push(commands.registerCommand(terminal_eval_selection_cmd, terminal_eval_selection_handler));
 
   const clear_cache_cmd = "imandrax.clear_cache";
-  const clear_cache_handler = () => { implementations.clear_cache(getClient); };
+  const clear_cache_handler = async () => { await implementations.clear_cache(getClient); };
   context.subscriptions.push(commands.registerCommand(clear_cache_cmd, clear_cache_handler));
 
   const open_vfs_file_cmd = "imandrax.open_vfs_file";
@@ -60,10 +60,10 @@ export function register(context: ExtensionContext, imandraxLanguageClient: Iman
   context.subscriptions.push(commands.registerCommand(open_goal_state_cmd, open_goal_state_handler));
 
   const reset_goal_state_cmd = "imandrax.reset_goal_state";
-  const reset_goal_state_handler = () => {
+  const reset_goal_state_handler = async () => {
     if (getClient()?.isRunning()) {
       try {
-        getClient().sendRequest("workspace/executeCommand", { "command": "reset-goal-state", "arguments": [] });
+        await getClient().sendRequest("workspace/executeCommand", { "command": "reset-goal-state", "arguments": [] });
       }
       catch (e) {
         console.log("caught something!");

src/extension.ts

@@ -11,8 +11,7 @@ import {
   ExtensionMode,
   Uri,
   window,
-  workspace,
-  TextEditorDecorationType
+  workspace
 } from "vscode";
 
 import {
@@ -21,10 +20,11 @@ import {
 
 
 export async function activate(context: ExtensionContext) {
-  const languageClientConfig = imandraxLanguageClient.configuration.get();
+  const getConfig = imandraxLanguageClient.configuration.get;
+  const languageClientConfig = getConfig();
 
   if (imandraxLanguageClient.configuration.isFoundPath(languageClientConfig)) {
-    const languageClientWrapper_ = new imandraxLanguageClient.ImandraxLanguageClient(languageClientConfig);
+    const languageClientWrapper_ = new imandraxLanguageClient.ImandraXLanguageClient(getConfig);
     const getClient: () => LanguageClient = () => { return languageClientWrapper_.getClient(); };
 
     formatter.register();
@@ -39,8 +39,8 @@ export async function activate(context: ExtensionContext) {
       (global as any).testListeners = listenersInstance;
     }
 
-    workspace.onDidChangeConfiguration(event => {
-      languageClientWrapper_.update_configuration(context.extensionUri, event);
+    workspace.onDidChangeConfiguration(async event => {
+      await languageClientWrapper_.update_configuration(context.extensionUri, event);
     });
 
     await languageClientWrapper_.start({ extensionUri: context.extensionUri });

src/imandrax_language_client/configuration.ts

@@ -24,8 +24,8 @@ type BinPathAvailability =
   }
 
 export interface ImandraXLanguageClientConfiguration {
-  serverArgs: any,
-  mergedEnv: any,
+  serverArgs: string[],
+  mergedEnv: object,
   binPathAvailability: BinPathAvailability,
 }
 

src/imandrax_language_client/imandrax_language_client.ts

@@ -1,28 +1,25 @@
 import * as commands from '../commands/commands';
 import * as decorations from '../decorations';
 import * as vfsProvider from '../vfs_provider';
-
-import { FoundPathConfig } from './configuration';
+import * as configuration from './configuration';
 
 import { ConfigurationChangeEvent, ExtensionContext, ExtensionMode, Uri, window, workspace, WorkspaceConfiguration } from 'vscode';
 import { Executable, LanguageClient, LanguageClientOptions } from 'vscode-languageclient/node';
 
-
 export * as configuration from './configuration';
 
-
 const MAX_RESTARTS = 10;
 
 export interface RestartParams {
   extensionUri: Uri
 }
 
-export class ImandraxLanguageClient {
-  private readonly serverOptions: Executable;
+export class ImandraXLanguageClient {
   private client!: LanguageClient;
   private readonly vfsProvider_: vfsProvider.VFSContentProvider;
   private restartCount = 0;
   private isInitial = () => { return this.client === undefined; };
+  private readonly getConfig: () => configuration.ImandraXLanguageClientConfiguration;
 
   getRestartCount(context: ExtensionContext) {
     if (context?.extensionMode === ExtensionMode.Test) {
@@ -38,22 +35,31 @@ export class ImandraxLanguageClient {
     return this.vfsProvider_;
   }
 
-  constructor(languageClientConfig: FoundPathConfig) {
-    this.serverOptions = {
-      command: languageClientConfig.binPathAvailability.path,
-      args: languageClientConfig.serverArgs,
-      options: { env: languageClientConfig.mergedEnv }
-    };
+  constructor(getConfig:()=>configuration.ImandraXLanguageClientConfiguration) {
+    this.getConfig = getConfig;
     this.vfsProvider_ = new vfsProvider.VFSContentProvider(() => { return this.getClient(); });
   }
 
   // Start language server
   async start(params: { extensionUri: Uri }): Promise<void> {
+    const config = this.getConfig();
+
+    if (!configuration.isFoundPath(config)) {
+      console.log("ImandraX binary not found, cannot start language server.");
+      return;
+    }
+
     const was_initial = this.isInitial();
     if (was_initial) {
       console.log("Starting ImandraX LSP server");
     }
 
+    const serverOptions: Executable = {
+      command: config.binPathAvailability.path,
+      args: config.serverArgs,
+      options: { env: config.mergedEnv }
+    };
+
     // Options to control the language client
     const clientOptions: LanguageClientOptions = {
       // Register the server for plain text documents
@@ -71,7 +77,7 @@ export class ImandraxLanguageClient {
     this.client = new LanguageClient(
       "imandrax_lsp",
       "ImandraX LSP",
-      this.serverOptions,
+      serverOptions,
       clientOptions
     );
 
@@ -86,7 +92,7 @@ export class ImandraxLanguageClient {
         (params) => { commands.visualize_decomp(extensionUri, params); });
       this.client.onNotification("$imandrax/vfs-file-changed",
         (params) => {
-          const uri = Uri.parse(params["uri"]);
+          const uri = Uri.parse(params.uri);
           this.vfsProvider_.onDidChangeEmitter.fire(uri);
         });
     }
@@ -131,9 +137,9 @@ export class ImandraxLanguageClient {
     if (event === undefined || event.affectsConfiguration('imandrax')) {
       const client = this.client;
       if (event && (
-        event.affectsConfiguration('imandrax.lsp.binary') ||
-        event.affectsConfiguration('imandrax.lsp.arguments') ||
-        event.affectsConfiguration('imandrax.lsp.environment'))) {
+        event.affectsConfiguration("imandrax.lsp.binary") ||
+        event.affectsConfiguration("imandrax.lsp.arguments") ||
+        event.affectsConfiguration("imandrax.lsp.environment"))) {
         await this.restart({ extensionUri: extensionUri });
       }
 

src/listeners.ts

@@ -1,6 +1,6 @@
 import * as decorations from './decorations';
 
-import { commands, DecorationOptions, DiagnosticSeverity, ExtensionContext, languages, StatusBarAlignment, StatusBarItem, TextEditor, ThemeColor, Uri, window } from 'vscode';
+import { commands, DecorationOptions, DiagnosticSeverity, ExtensionContext, languages, StatusBarAlignment, StatusBarItem, TextEditor, ThemeColor, Uri, window, DiagnosticChangeEvent } from 'vscode';
 import { LanguageClient } from 'vscode-languageclient/node';
 
 
@@ -39,21 +39,20 @@ export class Listeners {
   }
 
   diagnostics_for_editor(editor: TextEditor) {
-    let all_good: DecorationOptions[] = [];
-    const all_bad: DecorationOptions[] = [];
-    const doc = editor.document;
-    if (doc !== undefined) {
-      languages.getDiagnostics(doc.uri).forEach(d => {
+    if (editor) {
+      const uri = editor.document.uri;
+      let all_good: DecorationOptions[] = [];
+      const all_bad: DecorationOptions[] = [];
+      const diags = languages.getDiagnostics(uri);
+      diags.forEach(d => {
         if (d.source === "lsp") {
-          if (editor) {
-            const good = d.severity === DiagnosticSeverity.Information || d.severity === DiagnosticSeverity.Hint;
-            const range = d.range.with(d.range.start, d.range.start);
-            const decoration_options: DecorationOptions = { range: range };
-            if (good) {
-              all_good.push(decoration_options);
-            } else {
-              all_bad.push(decoration_options);
-            }
+          const good = d.severity === DiagnosticSeverity.Information || d.severity === DiagnosticSeverity.Hint;
+          const range = d.range.with(d.range.start, d.range.start);
+          const decoration_options: DecorationOptions = { range: range };
+          if (good) {
+            all_good.push(decoration_options);
+          } else {
+            all_bad.push(decoration_options);
           }
         }
       }
@@ -99,51 +98,47 @@ export class Listeners {
     }
   }
 
-  async diagnostic_listener() {
-    const editor = window.activeTextEditor;
-    if (editor !== undefined) {
-      const doc = editor.document;
-      if (doc !== undefined) {
-        if (doc.languageId === "imandrax") {
+  async diagnostic_listener(e: DiagnosticChangeEvent) {
+    await Promise.all(e.uris.map(async uri => {
+      const editor = window.visibleTextEditors.find(e => e.document.uri.path == uri.path)
+      if (editor) {
+        const doc = editor.document;
+        if (doc && doc.languageId === "imandrax") {
           this.diagnostics_for_editor(editor);
-          const file_uri = editor.document.uri;
-          if (file_uri.scheme === "file") {
-            await this.req_file_progress(file_uri);
+          if (doc.uri.scheme === "file") {
+            await this.req_file_progress(doc.uri);
           } else {
             this.file_progress_sbi.hide();
           }
         }
       }
     }
+    ));
   }
 
-  async active_editor_listener() {
-    const editor = window.activeTextEditor;
-    if (editor !== undefined) {
+  async active_editor_listener(editor: TextEditor | undefined) {
+    if (editor) {
       const doc = editor.document;
-      if (doc !== undefined) {
-        if (doc.languageId === "imandrax") {
-          this.diagnostics_for_editor(editor);
-          const file_uri = doc.uri;
-          if (file_uri.scheme === "file") {
-            if (this.getClient()?.isRunning()) {
-              await this.getClient().sendNotification("$imandrax/active-document", { "uri": file_uri.path });
-            }
-            await this.req_file_progress(file_uri);
-          }
-          else {
-            this.file_progress_sbi.hide();
+      if (doc && doc.languageId === "imandrax") {
+        this.diagnostics_for_editor(editor);
+        if (doc.uri.scheme === "file") {
+          if (this.getClient()?.isRunning()) {
+            await this.getClient().sendNotification("$imandrax/active-document", { "uri": doc.uri.path });
           }
+          await this.req_file_progress(doc.uri);
         }
         else {
           this.file_progress_sbi.hide();
         }
       }
+      else {
+        this.file_progress_sbi.hide();
+      }
     }
   }
 
   public register() {
-    languages.onDidChangeDiagnostics(async () => { await this.diagnostic_listener(); }, undefined, []);
-    window.onDidChangeActiveTextEditor(async () => { await this.active_editor_listener(); }, undefined, []);
+    languages.onDidChangeDiagnostics(async (e: DiagnosticChangeEvent) => { await this.diagnostic_listener(e); });
+    window.onDidChangeActiveTextEditor(async (e: TextEditor | undefined) => { await this.active_editor_listener(e); });
   }
 }