From ef9c87ac854efce7271c485a7d08867aae9f9f95 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Oct 2023 16:08:25 +0200 Subject: [PATCH] [lsp] Implement `textDocument/selectionRange`. We return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. Note the current implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. This could be of help for #580. --- CHANGES.md | 6 ++++++ controller/lsp_core.ml | 30 +++++++++++++++++++++++++++--- controller/request.ml | 2 ++ controller/request.mli | 2 ++ controller/rq_hover.ml | 2 +- controller/rq_init.ml | 1 + controller/rq_selectionRange.ml | 26 ++++++++++++++++++++++++++ controller/rq_selectionRange.mli | 18 ++++++++++++++++++ etc/doc/PROTOCOL.md | 1 + lsp/core.ml | 9 +++++++++ lsp/core.mli | 9 +++++++++ 11 files changed, 102 insertions(+), 4 deletions(-) create mode 100644 controller/rq_selectionRange.ml create mode 100644 controller/rq_selectionRange.mli diff --git a/CHANGES.md b/CHANGES.md index dbac0004..895093d4 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -48,6 +48,12 @@ - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, #573, helps with #558) + - Implement `textDocument/selectionRange` request, that will return + the range of the Coq sentence underlying the cursor. In VSCode, + this is triggered by the "Expand Selection" command. The + implementation is partial: we only take into account the first + position, and we only return a single range (Coq sentence) without + parents. (@ejgallego, #582) # coq-lsp 0.1.7: Just-in-time ----------------------------- diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 3980c0ef..6770bd04 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -25,7 +25,6 @@ module U = Yojson.Safe.Util let field name dict = List.(assoc name dict) let int_field name dict = U.to_int (field name dict) -let dict_field name dict = U.to_assoc (field name dict) let list_field name dict = U.to_list (field name dict) let string_field name dict = U.to_string (field name dict) let ofield name dict = List.(assoc_opt name dict) @@ -70,10 +69,18 @@ module Helpers = struct let Lsp.Doc.VersionedTextDocumentIdentifier.{ uri; version } = document in (uri, version) - let get_position params = - let pos = dict_field "position" params in + let lsp_position_to_tuple (pos : J.t) = + let pos = U.to_assoc pos in let line, character = (int_field "line" pos, int_field "character" pos) in (line, character) + + let get_position params = + let pos = field "position" params in + lsp_position_to_tuple pos + + let get_position_array params = + let pos_list = list_field "positions" params in + List.map lsp_position_to_tuple pos_list end (** LSP loop internal state: mainly the data needed to create a new document. In @@ -276,8 +283,24 @@ let do_position_request ~postpone ~params ~handler = Rq.Action.Data (Request.Data.PosRequest { uri; handler; point; version; postpone }) +(* For now we only pick the first item *) +let do_position_list_request ~postpone ~params ~handler = + let uri, version = Helpers.get_uri_oversion params in + let points = Helpers.get_position_array params in + match points with + | [] -> + let point, handler = ((0, 0), Request.empty) in + Rq.Action.Data + (Request.Data.PosRequest { uri; handler; point; version; postpone }) + | point :: _ -> + Rq.Action.Data + (Request.Data.PosRequest { uri; handler; point; version; postpone }) + let do_hover = do_position_request ~postpone:false ~handler:Rq_hover.hover +let do_selectionRange = + do_position_list_request ~postpone:false ~handler:Rq_selectionRange.request + (* We get the format from the params *) let get_pp_format_from_config () = match !Fleche.Config.v.pp_type with @@ -423,6 +446,7 @@ let dispatch_request ~method_ ~params : Rq.Action.t = | "textDocument/documentSymbol" -> do_symbols ~params | "textDocument/hover" -> do_hover ~params | "textDocument/codeLens" -> do_lens ~params + | "textDocument/selectionRange" -> do_selectionRange ~params (* Proof-specific stuff *) | "proof/goals" -> do_goals ~params (* Proof-specific stuff *) diff --git a/controller/request.ml b/controller/request.ml index 70c324ab..e6da1057 100644 --- a/controller/request.ml +++ b/controller/request.ml @@ -58,3 +58,5 @@ module Data = struct | PosRequest { uri = _; point; version = _; postpone = _; handler } -> handler ~point ~doc end + +let empty ~doc:_ ~point:_ = Ok (`List []) diff --git a/controller/request.mli b/controller/request.mli index d97c5a89..312cbfc6 100644 --- a/controller/request.mli +++ b/controller/request.mli @@ -42,3 +42,5 @@ module Data : sig val dm_request : t -> Fleche.Theory.Request.request val serve : doc:Fleche.Doc.t -> t -> R.t end + +val empty : position diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index a441d260..6d600f91 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -173,7 +173,7 @@ module type HoverProvider = sig end module Loc_info : HoverProvider = struct - let enabled = false + let enabled = true let h ~contents:_ ~point:_ ~node = match node with diff --git a/controller/rq_init.ml b/controller/rq_init.ml index eff20ec3..29a7adaf 100644 --- a/controller/rq_init.ml +++ b/controller/rq_init.ml @@ -128,6 +128,7 @@ let do_initialize ~params = ] ) ; ("definitionProvider", `Bool true) ; ("codeLensProvider", `Assoc []) + ; ("selectionRangeProvider", `Bool true) ; ( "workspace" , `Assoc [ ( "workspaceFolders" diff --git a/controller/rq_selectionRange.ml b/controller/rq_selectionRange.ml new file mode 100644 index 00000000..96016d4e --- /dev/null +++ b/controller/rq_selectionRange.ml @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Ok `Null + | Some node -> + let range = Fleche.Doc.Node.range node in + let parent = None in + let answer = Lsp.Core.SelectionRange.({ range; parent } |> to_yojson) in + Ok (`List [ answer ]) diff --git a/controller/rq_selectionRange.mli b/controller/rq_selectionRange.mli new file mode 100644 index 00000000..45983b03 --- /dev/null +++ b/controller/rq_selectionRange.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(*