[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

@@ -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
 -----------------------------

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 *)

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 [])

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

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

controller/rq_init.ml

@@ -128,6 +128,7 @@ let do_initialize ~params =
           ] )
     ; ("definitionProvider", `Bool true)
     ; ("codeLensProvider", `Assoc [])
+    ; ("selectionRangeProvider", `Bool true)
     ; ( "workspace"
       , `Assoc
           [ ( "workspaceFolders"

controller/rq_selectionRange.ml

@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+let request ~doc ~point =
+  let approx = Fleche.Info.Exact in
+  match Fleche.Info.LC.node ~doc ~point approx with
+  | None -> 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 ])

controller/rq_selectionRange.mli

@@ -0,0 +1,18 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+val request : Request.position

etc/doc/PROTOCOL.md

@@ -45,6 +45,7 @@ If a feature doesn't appear here it usually means it is not planned in the short
 | `textDocument/publishDiagnostics`     | Yes     |                                                            |
 | `textDocument/diagnostic`             | No      | Planned, issue #49                                         |
 | `textDocument/codeAction`             | No      | Planned                                                    |
+| `textDocument/selectionRange`         | Partial | We only take into account the first selection; no parents  |
 |---------------------------------------|---------|------------------------------------------------------------|
 | `workspace/workspaceFolders`          | Yes     | Each folder should have a `_CoqProject` file at the root.  |
 | `workspace/didChangeWorkspaceFolders` | Yes     |                                                            |

lsp/core.ml

@@ -115,6 +115,15 @@ module CodeLens = struct
   [@@deriving yojson]
 end
 
+(** SelectionRange *)
+module SelectionRange = struct
+  type t =
+    { range : Lang.Range.t
+    ; parent : t option [@default None]
+    }
+  [@@deriving yojson]
+end
+
 (** Pull Diagnostics *)
 module DocumentDiagnosticParams = struct
   type t =

lsp/core.mli

@@ -114,6 +114,15 @@ module CodeLens : sig
   [@@deriving yojson]
 end
 
+(** SelectionRange *)
+module SelectionRange : sig
+  type t =
+    { range : Lang.Range.t
+    ; parent : t option [@default None]
+    }
+  [@@deriving yojson]
+end
+
 (** Pull Diagnostics *)
 module DocumentDiagnosticParams : sig
   type t =