[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` (cc: #816)

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.

This commit switches `documentSymbols` to the immediate mode, when in
lazy checking 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