[lsp] Allow selectionRange call to take more than one position.

Fixes #663

CHANGES.md

@@ -65,6 +65,8 @@
    #348)
  - fix Coq performance view display (@ejgallego, #663, regression in
    #513)
+ - allow more than one input position in `selectionRange` LSP call
+   (@ejgallego, #667, fixes #663)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

controller/lsp_core.ml

@@ -306,7 +306,16 @@ 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 *)
+(* XXX Duplicate with theory.ml; inverse comparsion so larger points come
+   first *)
+let compare p1 p2 =
+  let x1, y1 = p1 in
+  let x2, y2 = p2 in
+  let xres = Int.compare x1 x2 in
+  if xres = 0 then -Int.compare y1 y2 else -xres
+
+(* A little bit hacky, but selectionRange is the only request that needs this...
+   so we will survive *)
 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
@@ -315,7 +324,9 @@ let do_position_list_request ~postpone ~params ~handler =
     let point, handler = ((0, 0), Request.empty) in
     Rq.Action.Data
       (Request.Data.PosRequest { uri; handler; point; version; postpone })
-  | point :: _ ->
+  | points ->
+    let handler = handler ~points in
+    let point = List.hd (List.sort compare points) in
     Rq.Action.Data
       (Request.Data.PosRequest { uri; handler; point; version; postpone })
 

controller/rq_selectionRange.ml

@@ -15,12 +15,19 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-let request ~token:_ ~doc ~point =
+let point_to_result ~doc ((line, character) as 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 ])
+  let range =
+    match Fleche.Info.LC.node ~doc ~point approx with
+    | None ->
+      let point = { Lang.Point.line; character; offset = -1 } in
+      { Lang.Range.start = point; end_ = point }
+    | Some node -> Fleche.Doc.Node.range node
+  in
+  let parent = None in
+  Lsp.Core.SelectionRange.{ range; parent }
+
+let request ~points ~token:_ ~doc ~point:_ =
+  let results = List.map (point_to_result ~doc) points in
+  let answers = List.map Lsp.Core.SelectionRange.to_yojson results in
+  Ok (`List answers)

controller/rq_selectionRange.mli

@@ -15,4 +15,4 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-val request : Request.position
+val request : points:(int * int) list -> Request.position

etc/doc/PROTOCOL.md

@@ -45,7 +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  |
+| `textDocument/selectionRange`         | Partial | Selection for a point is its span; no parents              |
 |---------------------------------------|---------|------------------------------------------------------------|
 | `workspace/workspaceFolders`          | Yes     | Each folder should have a `_CoqProject` file at the root.  |
 | `workspace/didChangeWorkspaceFolders` | Yes     |                                                            |