diff --git a/CHANGES.md b/CHANGES.md index e204c5b8..d8f3dd40 100644 --- a/CHANGES.md +++ b/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 ----------------------------- diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index c9c36765..8679846e 100644 --- a/controller/lsp_core.ml +++ b/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 diff --git a/controller/rq_init.ml b/controller/rq_init.ml index d0f5f606..d99a4db6 100644 --- a/controller/rq_init.ml +++ b/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 ( diff --git a/controller/rq_init.mli b/controller/rq_init.mli index 39909178..c4a424c5 100644 --- a/controller/rq_init.mli +++ b/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 diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 76bd46a0..03fae8ae 100644 --- a/editor/code/src/client.ts +++ b/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); diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index 5ef7a380..1b933a80 100644 --- a/etc/doc/PROTOCOL.md +++ b/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> 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.