diff --git a/client/package.json b/client/package.json index f34b7e51..81a53a8e 100644 --- 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 index 0dab0c95..bc902897 100644 --- 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 index 75012025..3eb86610 100644 --- 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 index 5d9d5d23..3d0a157c 100644 --- 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 index 9cf0fd49..8930885b 100644 --- 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