[lsp] Update server settings on the fly.

CHANGES.md

@@ -108,6 +108,10 @@
  - New server option to enable / disable `coq/perfData` (@ejgallego, #689)
  - The `coq-lsp.document` VSCode command will now display the returned
    JSON data in a new editor (@ejgallego, #701)
+ - New server option to enable / disable `coq/perfData` (@ejgallego,
+   #689)
+ - Update server settings on the fly when tweaking them in VSCode.
+   Implement `workspace/didChangeConfiguration` (@ejgallego, #702)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

controller/lsp_core.ml

@@ -406,6 +406,13 @@ let do_cancel ~ofn ~params =
 
 let do_cache_trim () = Nt_cache_trim.notification ()
 
+let do_changeConfiguration params =
+  let message = "didChangeReceived" in
+  let () = LIO.(logMessage ~lvl:Lvl.Info ~message) in
+  let settings = field "settings" params |> U.to_assoc in
+  Rq_init.do_settings settings;
+  ()
+
 (***********************************************************************)
 
 (** LSP Init routine *)
@@ -469,8 +476,9 @@ let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit =
   match method_ with
   (* Lifecycle *)
   | "exit" -> raise Lsp_exit
-  (* setTrace *)
+  (* setTrace and settings *)
   | "$/setTrace" -> do_trace params
+  | "workspace/didChangeConfiguration" -> do_changeConfiguration params
   (* Document lifetime *)
   | "textDocument/didOpen" -> do_open ~io ~token ~state params
   | "textDocument/didChange" -> do_change ~io ~ofn ~token params

controller/rq_init.ml

@@ -24,9 +24,9 @@ let odict_field name dict =
     []
 
 (* Request Handling: The client expects a reply *)
-let do_client_options coq_lsp_options : unit =
-  LIO.trace "init" "custom client options:";
-  LIO.trace_object "init" (`Assoc coq_lsp_options);
+let do_settings coq_lsp_options : unit =
+  LIO.trace "settings" "setting server options:";
+  LIO.trace_object "settings" (`Assoc coq_lsp_options);
   match Lsp.JFleche.Config.of_yojson (`Assoc coq_lsp_options) with
   | Ok v -> Fleche.Config.v := v
   | Error msg -> LIO.trace "CoqLspOption.of_yojson error: " msg
@@ -109,8 +109,8 @@ let do_initialize ~params =
   let dir = determine_workspace_root ~params in
   let trace = get_trace ~params in
   LIO.set_trace_value trace;
-  let coq_lsp_options = odict_field "initializationOptions" params in
-  do_client_options coq_lsp_options;
+  let coq_lsp_settings = odict_field "initializationOptions" params in
+  do_settings coq_lsp_settings;
   check_client_version !Fleche.Config.v.client_version;
   let client_capabilities = odict_field "capabilities" params in
   if Fleche.Debug.lsp_init then (

controller/rq_init.mli

@@ -5,6 +5,9 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+(** Setups the server configuration, takes the list of settings as a JSON dict *)
+val do_settings : (string * Yojson.Safe.t) list -> unit
+
 (** Returns answer request + workspace root directory *)
 val do_initialize :
   params:(string * Yojson.Safe.t) list -> Yojson.Safe.t * string list

editor/code/src/client.ts

@@ -18,6 +18,8 @@ import {
 
 import {
   BaseLanguageClient,
+  DidChangeConfigurationNotification,
+  DidChangeConfigurationParams,
   LanguageClientOptions,
   NotificationType,
   RequestType,
@@ -80,19 +82,27 @@ export function activateCoqLSP(
 ): CoqLspAPI {
   window.showInformationMessage("Coq LSP Extension: Going to activate!");
 
-  workspace.onDidChangeConfiguration((cfgChange) => {
-    if (cfgChange.affectsConfiguration("coq-lsp")) {
-      // Refactor to remove the duplicate call below
-      const wsConfig = workspace.getConfiguration("coq-lsp");
-      config = CoqLspClientConfig.create(wsConfig);
+  // Update config on client and server
+  function configDidChange(wsConfig: any): CoqLspServerConfig {
+    config = CoqLspClientConfig.create(wsConfig);
+    let client_version = context.extension.packageJSON.version;
+    let settings = CoqLspServerConfig.create(client_version, wsConfig);
+    let params: DidChangeConfigurationParams = { settings };
+
+    if (client && client.isRunning()) {
+      let type = DidChangeConfigurationNotification.type;
+      client.sendNotification(type, params);
     }
-  });
+
+    return settings;
+  }
 
   function coqCommand(command: string, fn: () => void) {
     let disposable = commands.registerCommand("coq-lsp." + command, fn);
     context.subscriptions.push(disposable);
   }
   function coqEditorCommand(command: string, fn: (editor: TextEditor) => void) {
+    // EJGA: we should check for document selector here.
     let disposable = commands.registerTextEditorCommand(
       "coq-lsp." + command,
       fn
@@ -143,13 +153,9 @@ export function activateCoqLSP(
     if (client && client.isRunning()) return;
 
     const wsConfig = workspace.getConfiguration("coq-lsp");
-    config = CoqLspClientConfig.create(wsConfig);
 
-    let client_version = context.extension.packageJSON.version;
-    const initializationOptions = CoqLspServerConfig.create(
-      client_version,
-      wsConfig
-    );
+    // This also sets `config` variable
+    const initializationOptions: CoqLspServerConfig = configDidChange(wsConfig);
 
     const clientOptions: LanguageClientOptions = {
       documentSelector: CoqSelector.local,
@@ -205,6 +211,17 @@ export function activateCoqLSP(
   // Check VSCoq is not installed
   checkForVSCoq();
 
+  // Config change events setup
+  let onDidChange = workspace.onDidChangeConfiguration((cfgChange) => {
+    if (cfgChange.affectsConfiguration("coq-lsp")) {
+      // Refactor to remove the duplicate call below
+      const wsConfig = workspace.getConfiguration("coq-lsp");
+      configDidChange(wsConfig);
+    }
+  });
+
+  context.subscriptions.push(onDidChange);
+
   // InfoPanel setup.
   infoPanel = new InfoPanel(context.extensionUri);
   context.subscriptions.push(infoPanel);

etc/doc/PROTOCOL.md

@@ -52,6 +52,7 @@ If a feature doesn't appear here it usually means it is not planned in the short
 |---------------------------------------|---------|------------------------------------------------------------|
 | `workspace/workspaceFolders`          | Yes     | Each folder should have a `_CoqProject` file at the root.  |
 | `workspace/didChangeWorkspaceFolders` | Yes     |                                                            |
+| `workspace/didChangeConfiguration`    | Yes (*) | We still do a client -> server push, instead of pull       |
 |---------------------------------------|---------|------------------------------------------------------------|
 
 ### URIs accepted by coq-lsp
@@ -352,3 +353,38 @@ const coqPerfData : NotificationType<DocumentPerfParams<Range>>
 
 The `coq/trimCaches` notification from client to server tells the
 server to free memory. It has no parameters.
+
+### Did Change Configuration and Server Configuration parameters
+
+The server will listen to the `workspace/didChangeConfiguration`
+parameters and try to update them without a full server restart.
+
+The `settings` field corresponds to the data structure also passed in
+the `initializationOptions` parameter for the LSP `init` method.
+
+As of today, the server exposes the following parameters:
+
+```typescript
+export interface CoqLspServerConfig {
+  client_version: string;
+  eager_diagnostics: boolean;
+  goal_after_tactic: boolean;
+  show_coq_info_messages: boolean;
+  show_notices_as_diagnostics: boolean;
+  admit_on_bad_qed: boolean;
+  debug: boolean;
+  unicode_completion: "off" | "normal" | "extended";
+  max_errors: number;
+  pp_type: 0 | 1 | 2;
+  show_stats_on_hover: boolean;
+  show_loc_info_on_hover: boolean;
+  check_only_on_request: boolean;
+}
+```
+
+The settings are documented in the `package.json` file for the VSCode
+client.
+
+#### Changelog
+
+- v0.1.9: First public documentation.