[lsp] Support client-side setting of server options.

This is very convenient as for the user to be able to set server options that currently require a recompile.
ejgallego · Nov 14, 2022 · f7525de · f7525de
1 parent 276a63c
commit f7525de
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 14 deletions.
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
@@ -30,7 +30,7 @@ let _option_empty x =
   | None -> true
   | Some _ -> false
 
-let option_cata f x d =
+let option_cata f d x =
   match x with
   | None -> d
   | Some x -> f x
@@ -40,29 +40,64 @@ let option_default x d =
   | None -> d
   | Some x -> x
 
-let oint_field name dict = option_cata U.to_int List.(assoc_opt name dict) 0
+let oint_field name dict = option_cata U.to_int 0 List.(assoc_opt name dict)
+let ostring_field name dict = Option.map U.to_string (List.assoc_opt name dict)
 
 let odict_field name dict =
   option_default
     U.(to_option to_assoc (option_default List.(assoc_opt name dict) `Null))
     []
 
+module TraceValue = struct
+  type t =
+    | Off
+    | Messages
+    | Verbose
+
+  let parse = function
+    | "messages" -> Messages
+    | "verbose" -> Verbose
+    | "off" -> Off
+    | _ -> raise (Invalid_argument "TraceValue.parse")
+
+  let to_string = function
+    | Off -> "off"
+    | Messages -> "messages"
+    | Verbose -> "verbose"
+end
+
 module LIO = Lsp.Io
 module LSP = Lsp.Base
 
 (* Request Handling: The client expects a reply *)
-let do_initialize ofmt ~id _params =
+let do_initialize ofmt ~id params =
+  let coq_lsp_options = odict_field "initializationOptions" params in
+  LIO.log_error "init" "custom client options:";
+  LIO.log_object "init" (`Assoc coq_lsp_options);
+  let client_capabilities = odict_field "capabilities" params in
+  LIO.log_error "init" "client capabilities:";
+  LIO.log_object "init" (`Assoc client_capabilities);
+  let trace =
+    ostring_field "trace" params |> option_cata TraceValue.parse TraceValue.Off
+  in
+  LIO.log_error "init" ("trace: " ^ TraceValue.to_string trace);
+  let capabilities =
+    [ ("textDocumentSync", `Int 1)
+    ; ("documentSymbolProvider", `Bool true)
+    ; ("hoverProvider", `Bool true)
+    ; ("completionProvider", `Assoc [])
+    ; ("codeActionProvider", `Bool false)
+    ]
+  in
   let msg =
     LSP.mk_reply ~id
       ~result:
         (`Assoc
-          [ ( "capabilities"
+          [ ("capabilities", `Assoc capabilities)
+          ; ( "serverInfo"
             , `Assoc
-                [ ("textDocumentSync", `Int 1)
-                ; ("documentSymbolProvider", `Bool true)
-                ; ("hoverProvider", `Bool true)
-                ; ("completionProvider", `Assoc [])
-                ; ("codeActionProvider", `Bool false)
+                [ ("name", `String "coq-lsp (C) Inria 2022")
+                ; ("version", `String "0.1+alpha")
                 ] )
           ])
   in

diff --git a/editor/code/package.json b/editor/code/package.json
@@ -87,6 +87,16 @@
             "items": { "type": "string" },
             "default": [ "--std" ],
             "description": "Arguments to the coq-lsp server"
+          },
+          "coq-lsp.eager_diagnostics": {
+            "type": "boolean",
+            "default": true,
+            "description": "Send diagnostics as document is processed; if false, diagnostics are only sent when Coq finishes processing the file"
+          },
+          "coq-lsp.ok_diagnostics": {
+            "type": "boolean",
+            "default": false,
+            "description": "Send a diagnostic for sentences that are Ok; this can choke vsCode easily due to too many diagnostics"
           }
         }
       }

diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
@@ -6,11 +6,6 @@ let client : LanguageClient;
 export function activate (context : ExtensionContext) : void {
     window.showInformationMessage('Going to activate!');
 
-    const clientOptions = {
-        documentSelector: [
-            {scheme: 'file', language: 'coq'}
-        ]
-    };
     function coqCommand(command : string, fn : () => void) {
         let disposable = commands.registerCommand('coq-lsp.'+command, fn);
         context.subscriptions.push(disposable);
@@ -22,6 +17,17 @@ export function activate (context : ExtensionContext) : void {
         window.showInformationMessage('Going to start!');
 
         const config = workspace.getConfiguration('coq-lsp');
+        const initializationOptions = {
+            eager_diagnostics: config.eager_diagnostics,
+            ok_diagnostics: config.ok_diagnostics
+        };
+
+        const clientOptions = {
+            documentSelector: [
+                {scheme: 'file', language: 'coq'}
+            ],
+            initializationOptions
+        };
         const serverOptions = { command: config.path, args: config.args };
 
         client = new LanguageClient(