Merge pull request #527 from coq-community/completion-settings

Add setting to enable/disable completion
coq · Aug 1, 2023 · 5ec155a · 5ec155a
2 parents c393825 + 934e45d
commit 5ec155a
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 2 deletions.
diff --git a/client/package.json b/client/package.json
@@ -156,6 +156,12 @@
         "title": "Code Completion",
         "type": "object",
         "properties": {
+          "vscoq.completion.enable": {
+            "scope": "window",
+            "type": "boolean",
+            "default": false,
+            "description": "Enable completion support from the VsCoq language server"
+          },
           "vscoq.completion.unificationLimit": {
             "scope": "window",
             "type": "number",

diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
@@ -47,6 +47,7 @@ type options = {
 let default_options = {
   delegation_mode = CheckProofsInMaster;
   completion_options = {
+    enable = false;
     algorithm = StructuredSplitUnification;
     unificationLimit = 100;
     atomicFactor = 5.;

diff --git a/language-server/lsp/lspData.ml b/language-server/lsp/lspData.ml
@@ -264,6 +264,7 @@ module Settings = struct
     end
 
     type t = {
+      enable: bool;
       algorithm: RankingAlgoritm.t;
       unificationLimit: int;
       atomicFactor: float [@default 5.]; (** Controls how highly specific types are prioritised over generics *)

diff --git a/language-server/tests/em_tests.ml b/language-server/tests/em_tests.ml
@@ -23,7 +23,7 @@ let uri = Uri.make ~scheme:"file" ~path:"foo" ()
 let init text = openDoc uri ~text
 
 let set_delegation_mode mode =
-  ExecutionManager.(set_options { delegation_mode = mode; completion_options = { unificationLimit = 100; algorithm = StructuredSplitUnification; atomicFactor = 5.; sizeFactor = 5. }; enableDiagnostics = true })
+  ExecutionManager.(set_options { delegation_mode = mode; completion_options = { enable = false; unificationLimit = 100; algorithm = StructuredSplitUnification; atomicFactor = 5.; sizeFactor = 5. }; enableDiagnostics = true })
 
 let%test_unit "exec: finished proof" =
   let st, init_events = init "Lemma x : True. trivial. Qed. Check x." in

diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
@@ -292,8 +292,10 @@ let coqtopStepForward params =
       filterText = (if label == insertText then None else Some (insertText));
     } 
 
-
 let textDocumentCompletion ~id params =
+  if not (Dm.ExecutionManager.get_options ()).completion_options.enable then
+    Ok Request.Client.CompletionResult.{ isIncomplete = false; items = [] }, []
+  else
   let Request.Client.CompletionParams.{ textDocument = { uri }; position } = params in
   let st = Hashtbl.find states (Uri.path uri) in
   match Dm.DocumentManager.get_completions st position with