Merge pull request #841 from ejgallego/request_imm

[fleche] New immediate request serving mode.

CHANGES.md

@@ -25,6 +25,15 @@
    @corwin-of-amber, #433)
  - [hover] Fix universe and level printing in hover (#839, fixes #835
    , @ejgallego , @Alizter)
+ - [fleche] New immediate request serving mode. In this mode, requests
+   are served with whatever document state we have. This is very
+   useful when we are not in continuous mode, and we don't have a good
+   reference as to what to build, for example in
+   `documentSymbols`. The mode actually works pretty well in practice
+   as often language requests will come after goals requests, so the
+   info that is needed is at hand. It could also be tried to set the
+   build target for immediate requests to the view hint, but we should
+   see some motivation for that (@ejgallego, #841)
 
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------

controller/lsp_core.ml

@@ -402,7 +402,16 @@ let do_document_request_maybe ~params ~handler =
   let postpone = not !Fleche.Config.v.check_only_on_request in
   do_document_request ~postpone ~params ~handler
 
-let do_symbols = do_document_request_maybe ~handler:Rq_symbols.symbols
+let do_immediate ~params ~handler =
+  let uri = Helpers.get_uri params in
+  Rq.Action.Data (Request.Data.Immediate { uri; handler })
+
+(* new immediate mode, cc: #816 *)
+let do_symbols ~params =
+  let handler = Rq_symbols.symbols in
+  if !Fleche.Config.v.check_only_on_request then do_immediate ~params ~handler
+  else do_document_request ~postpone:true ~params ~handler
+
 let do_document = do_document_request_maybe ~handler:Rq_document.request
 let do_save_vo = do_document_request_maybe ~handler:Rq_save.request
 let do_lens = do_document_request_maybe ~handler:Rq_lens.request

controller/request.ml

@@ -48,6 +48,10 @@ type position =
 (** Requests that require data access *)
 module Data = struct
   type t =
+    | Immediate of
+        { uri : Lang.LUri.File.t
+        ; handler : document
+        }
     | DocRequest of
         { uri : Lang.LUri.File.t
         ; postpone : bool
@@ -63,6 +67,7 @@ module Data = struct
 
   (* Debug printing *)
   let data fmt = function
+    | Immediate { uri = _; handler = _ } -> Format.fprintf fmt "{k:imm }"
     | DocRequest { uri = _; postpone; handler = _ } ->
       Format.fprintf fmt "{k:doc | p: %B}" postpone
     | PosRequest { uri = _; point; version; postpone; handler = _ } ->
@@ -73,13 +78,16 @@ module Data = struct
 
   let dm_request pr =
     match pr with
+    | Immediate { uri; handler = _ } ->
+      (uri, false, Fleche.Theory.Request.Immediate)
     | DocRequest { uri; postpone; handler = _ } ->
       (uri, postpone, Fleche.Theory.Request.FullDoc)
     | PosRequest { uri; point; version; postpone; handler = _ } ->
       (uri, postpone, Fleche.Theory.Request.(PosInDoc { point; version }))
 
   let serve ~token ~doc pr =
     match pr with
+    | Immediate { uri = _; handler } -> handler ~token ~doc
     | DocRequest { uri = _; postpone = _; handler } -> handler ~token ~doc
     | PosRequest { uri = _; point; version = _; postpone = _; handler } ->
       handler ~token ~point ~doc

controller/request.mli

@@ -35,6 +35,10 @@ type position =
 (** Requests that require data access *)
 module Data : sig
   type t =
+    | Immediate of
+        { uri : Lang.LUri.File.t
+        ; handler : document
+        }
     | DocRequest of
         { uri : Lang.LUri.File.t
         ; postpone : bool

fleche/theory.ml

@@ -341,6 +341,7 @@ let close ~uri =
 
 module Request = struct
   type request =
+    | Immediate
     | FullDoc
     | PosInDoc of
         { point : int * int
@@ -379,6 +380,7 @@ module Request = struct
     let default () = Cancel in
     (* should be Cancelled? *)
     match request with
+    | Immediate -> Handle.with_doc ~kind ~default ~uri ~f:(fun _ doc -> Now doc)
     | FullDoc ->
       Handle.with_doc ~kind ~default ~uri ~f:(fun _ doc ->
           match (Doc.Completion.is_completed doc.completed, postpone) with
@@ -402,6 +404,7 @@ module Request = struct
   (** Removes the request from the list of things to wake up *)
   let remove { id; uri; postpone = _; request } =
     match request with
+    | Immediate -> ()
     | FullDoc -> Handle.remove_cp_request ~uri ~id
     | PosInDoc { point; _ } -> Handle.remove_pt_request ~uri ~id ~point
 end

fleche/theory.mli

@@ -49,6 +49,7 @@ val close : uri:Lang.LUri.File.t -> unit
 
 module Request : sig
   type request =
+    | Immediate
     | FullDoc
     | PosInDoc of
         { point : int * int