[controller] Allow to postpone and cancel requests

Some requests need to be delayed until the document is ready, such as
`documentSymbols`. In order to do this, we allow to postpone requests,
and `Doc_manager.check` will now return the list of requests pending
for a given document.

The implementation is lightweight and quite a prototype, but should
serve as a basis for more advanced stuff.

Closes #124.

CHANGES.md

@@ -12,6 +12,9 @@
  - `coq-lsp` will now warn the user when two files have been opened
    simultaneously and the parser may go into a broken state :/
    (@ejgallego #169)
+ - Implement request postponement and cancellation. Thus
+   `documentSymbols` will now be postponed until the document is
+   ready, (@ejgallego #141, fixes #124)
 
 # coq-lsp 0.1.2: Message
 ------------------------

controller/coq_lsp.ml

@@ -57,6 +57,19 @@ module LIO = Lsp.Io
 module LSP = Lsp.Base
 module Check = Doc_manager.Check
 
+module PendingRequest = struct
+  type t = { uri : string; handler: uri:string -> doc:Fleche.Doc.t -> J.t }
+end
+
+module RResult = struct
+  type t =
+    | Ok of Yojson.Safe.t
+    | Error of int * string
+    | Postpone of PendingRequest.t
+
+  let ok x = Ok x
+end
+
 (* Request Handling: The client expects a reply *)
 module CoqLspOption = struct
   type t = [%import: Fleche.Config.t] [@@deriving yojson]
@@ -108,9 +121,9 @@ let do_initialize ~params =
           ; ("version", `String Version.server)
           ] )
     ]
-  |> Result.ok
+  |> RResult.ok
 
-let do_shutdown ~params:_ = Ok `Null
+let do_shutdown ~params:_ = RResult.Ok `Null
 
 let do_open ~state params =
   let document = dict_field "textDocument" params in
@@ -153,10 +166,6 @@ let get_position params =
   let line, character = (int_field "line" pos, int_field "character" pos) in
   (line, character)
 
-let do_document_request ~params ~handler =
-  let uri, doc = get_textDocument params in
-  handler ~uri ~doc
-
 let do_position_request ~params ~handler =
   let _uri, doc = get_textDocument params in
   let point = get_position params in
@@ -168,18 +177,26 @@ let do_position_request ~params ~handler =
       line < loc.line_nb_last
       || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last)
   in
-  if in_range then Result.Ok (handler ~doc ~point)
+  if in_range then RResult.Ok (handler ~doc ~point)
   else
     (* -32802 = RequestFailed | -32803 = ServerCancelled ; *)
     let code = -32802 in
     let message = "Document is not ready" in
-    Result.Error (code, message)
+    RResult.Error (code, message)
 
-let do_symbols = do_document_request ~handler:Requests.symbols
 let do_hover = do_position_request ~handler:Requests.hover
 let do_goals = do_position_request ~handler:Requests.goals
 let do_completion = do_position_request ~handler:Requests.completion
 
+(* Requires the full document to be processed *)
+let do_document_request ~params ~handler =
+  let uri, doc = get_textDocument params in
+  match doc.completed with
+  | Yes _ -> RResult.Ok (handler ~uri ~doc)
+  | Stopped _ | Failed _ -> Postpone { uri; handler }
+
+let do_symbols = do_document_request ~handler:Requests.symbols
+
 let do_trace params =
   let trace = string_field "value" params in
   LIO.set_trace_value (LIO.TraceValue.of_string trace)
@@ -196,11 +213,36 @@ let rec read_request ic =
     LIO.trace "read_request" ("error: " ^ msg);
     read_request ic
 
+let rtable : (int, PendingRequest.t) Hashtbl.t = Hashtbl.create 673
+
 let answer_request ofmt ~id result =
-  (match result with
-  | Ok result -> LSP.mk_reply ~id ~result
-  | Error (code, message) -> LSP.mk_request_error ~id ~code ~message)
-  |> LIO.send_json ofmt
+  match result with
+  | RResult.Ok result -> LSP.mk_reply ~id ~result |> LIO.send_json ofmt
+  | Error (code, message) ->
+    LSP.mk_request_error ~id ~code ~message |> LIO.send_json ofmt
+  | Postpone ({ uri; _ } as pr) ->
+    Doc_manager.serve_on_completion ~uri ~id;
+    Hashtbl.add rtable id pr
+
+let do_cancel ofmt ~params =
+  let id = int_field "id" params in
+  Hashtbl.remove rtable id;
+  answer_request ofmt ~id (Error (-32800, "Cancelled by client"))
+
+let serve_postponed_request id =
+  match Hashtbl.find_opt rtable id with
+  | None -> LIO.trace "can't serve cancelled request: " (string_of_int id); None
+  | Some { uri; handler } ->
+    LIO.trace "serving rq: " (string_of_int id ^ " uri: " ^ uri);
+    Hashtbl.remove rtable id;
+    let doc = Doc_manager.find_doc ~uri in
+    Some (RResult.Ok (handler ~uri ~doc))
+
+let serve_postponed_request ofmt id =
+  serve_postponed_request id |> Option.iter (answer_request ofmt ~id)
+
+let serve_postponed_requests ofmt rl =
+  Int.Set.iter (serve_postponed_request ofmt) rl
 
 (***********************************************************************)
 
@@ -246,6 +288,8 @@ let dispatch_notification ofmt ~state ~method_ ~params =
   | "textDocument/didChange" -> do_change params
   | "textDocument/didClose" -> do_close ofmt params
   | "textDocument/didSave" -> Cache.save_to_disk ()
+  (* Cancel Request *)
+  | "$/cancelRequest" -> do_cancel ofmt ~params
   (* NOOPs *)
   | "initialized" -> ()
   (* Generic handler *)
@@ -255,8 +299,9 @@ let dispatch_request ~method_ ~params =
   match method_ with
   (* Lifecyle *)
   | "initialize" ->
-    (* XXX This can't happen here *)
-    do_initialize ~params
+    LIO.trace "dispatch_request" "duplicate initialize request! Rejecting";
+    (* XXX what's the error code here *)
+    RResult.Error (-32600, "Invalid Request: server already initialized")
   | "shutdown" -> do_shutdown ~params
   (* Symbols and info about the document *)
   | "textDocument/completion" -> do_completion ~params
@@ -309,20 +354,24 @@ let dispatch_message ofmt ~state com =
 (** Main event queue *)
 let request_queue = Queue.create ()
 
-let rec process_queue ofmt ~state =
-  if Fleche.Debug.sched_wakeup then
-    LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
-  (match Queue.peek_opt request_queue with
+let dispatch_or_resume_check ofmt ~state =
+  match Queue.peek_opt request_queue with
   | None ->
     Control.interrupt := false;
-    Check.check_or_yield ofmt ~fb_queue:state.State.fb_queue
+    let ready = Check.check_or_yield ofmt ~fb_queue:state.State.fb_queue in
+    serve_postponed_requests ofmt ready
   | Some com ->
     (* TODO: optimize the queue? *)
     ignore (Queue.pop request_queue);
     LIO.trace "process_queue" ("Serving Request: " ^ LSP.Message.method_ com);
     (* We let Coq work normally now *)
     Control.interrupt := false;
-    dispatch_message ofmt ~state com);
+    dispatch_message ofmt ~state com
+
+let rec process_queue ofmt ~state =
+  if Fleche.Debug.sched_wakeup then
+    LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
+  dispatch_or_resume_check ofmt ~state;
   process_queue ofmt ~state
 
 let process_input (com : LSP.Message.t) =

controller/doc_manager.ml

@@ -24,7 +24,11 @@ exception AbortRequest
 module Handle = struct
   type t =
     { doc : Fleche.Doc.t
-    ; requests : unit (* placeholder for requests attached to a document *)
+    ; requests : Int.Set.t
+          (* For now we just store the request id to wake up on completion,
+             later on we may want to store a more interesting type, for example
+             "wake up when a location is reached", or always to continue the
+             streaming *)
     }
 
   let doc_table : (string, t) Hashtbl.t = Hashtbl.create 39
@@ -34,7 +38,7 @@ module Handle = struct
     | None -> ()
     | Some _ ->
       LIO.trace "do_open" ("file " ^ uri ^ " not properly closed by client"));
-    Hashtbl.add doc_table uri { doc; requests = () }
+    Hashtbl.add doc_table uri { doc; requests = Int.Set.empty }
 
   let close ~uri = Hashtbl.remove doc_table uri
 
@@ -48,16 +52,34 @@ module Handle = struct
   let find_opt ~uri = Hashtbl.find_opt doc_table uri
   let find_doc ~uri = (find ~uri).doc
 
-  let _update ~handle ~(doc : Fleche.Doc.t) =
+  let _update_doc ~handle ~(doc : Fleche.Doc.t) =
     Hashtbl.replace doc_table doc.uri { handle with doc }
 
   (* Clear requests *)
   let update_doc_version ~(doc : Fleche.Doc.t) =
-    Hashtbl.replace doc_table doc.uri { doc; requests = () }
+    Hashtbl.replace doc_table doc.uri { doc; requests = Int.Set.empty }
+
+  let attach_request ~uri ~id =
+    match Hashtbl.find_opt doc_table uri with
+    | Some { doc; requests } ->
+      let requests = Int.Set.add id requests in
+      Hashtbl.replace doc_table uri { doc; requests }
+    | None -> ()
+
+  (* For now only on completion, I think we want check to return the list of
+     requests that can be served / woken up *)
+  let do_requests ~doc ~handle =
+    let handle = { handle with doc } in
+    match doc.completed with
+    | Yes _ -> ({ doc; requests = Int.Set.empty }, handle.requests)
+    | Stopped _ -> (handle, Int.Set.empty)
+    | Failed _ -> (handle, Int.Set.empty)
 
   (* trigger pending incremental requests *)
   let update_doc_info ~handle ~(doc : Fleche.Doc.t) =
-    Hashtbl.replace doc_table doc.uri { handle with doc }
+    let handle, requests = do_requests ~doc ~handle in
+    Hashtbl.replace doc_table doc.uri handle;
+    requests
 end
 
 let diags_of_doc doc =
@@ -78,21 +100,24 @@ module Check = struct
     match Handle.find_opt ~uri with
     | Some handle ->
       let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc ~fb_queue in
-      Handle.update_doc_info ~handle ~doc;
+      let requests = Handle.update_doc_info ~handle ~doc in
       let diags = diags_of_doc doc in
       let diags =
         Lsp_util.lsp_of_diags ~uri:doc.uri ~version:doc.version diags
       in
       LIO.send_json ofmt @@ diags;
       (* Only if completed! *)
-      if completed ~uri then pending := None
+      if completed ~uri then pending := None;
+      requests
     | None ->
       LIO.trace "Check.check" ("file " ^ uri ^ " not available");
-      ()
+      Int.Set.empty
 
   let check_or_yield ofmt ~fb_queue =
     match !pending with
-    | None -> Thread.delay 0.1
+    | None ->
+      Thread.delay 0.1;
+      Int.Set.empty
     | Some uri -> check ofmt ~fb_queue ~uri
 
   let schedule ~uri = pending := Some uri
@@ -145,3 +170,4 @@ let change ~uri ~version ~contents =
 
 let close = Handle.close
 let find_doc = Handle.find_doc
+let serve_on_completion ~uri ~id = Handle.attach_request ~uri ~id

controller/doc_manager.mli

@@ -17,9 +17,10 @@
 
 module Check : sig
   (** Check a document, or yield if there is none pending; it will send progress
-      and diagnostics notifications to [ofmt] *)
+      and diagnostics notifications to [ofmt]. Will return the list of requests
+      that are ready to execute. *)
   val check_or_yield :
-    Format.formatter -> fb_queue:Coq.Message.t list ref -> unit
+    Format.formatter -> fb_queue:Coq.Message.t list ref -> Int.Set.t
 end
 
 (** Create a document *)
@@ -41,3 +42,6 @@ exception AbortRequest
 
 (** [find_doc ~uri] , raises AbortRequest if [uri] is invalid *)
 val find_doc : uri:string -> Fleche.Doc.t
+
+(** Request support *)
+val serve_on_completion : uri:string -> id:int -> unit

controller/requests.ml

@@ -15,9 +15,7 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-type document_request =
-  uri:string -> doc:Fleche.Doc.t -> (Yojson.Safe.t, int * string) Result.t
-
+type document_request = uri:string -> doc:Fleche.Doc.t -> Yojson.Safe.t
 type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t
 
 module Util = struct
@@ -44,18 +42,10 @@ let _kind_of_type _tm = 13
    *) | _ -> 12 (* Function *) *)
 
 let symbols ~uri ~(doc : Fleche.Doc.t) =
-  match doc.completed with
-  | Yes _ ->
-    let f loc id = mk_syminfo uri (Names.Id.to_string id, "", 12, loc) in
-    let ast = Util.asts_of_doc doc in
-    let slist = Coq.Ast.grab_definitions f ast in
-    let result = `List slist in
-    Ok result
-  | Stopped _ | Failed _ ->
-    (* -32802 = RequestFailed | -32803 = ServerCancelled ; *)
-    let code = -32802 in
-    let message = "Document is not ready" in
-    Error (code, message)
+  let f loc id = mk_syminfo uri (Names.Id.to_string id, "", 12, loc) in
+  let ast = Util.asts_of_doc doc in
+  let slist = Coq.Ast.grab_definitions f ast in
+  `List slist
 
 let hover ~doc ~point =
   let show_loc_info = true in

controller/requests.mli

@@ -15,9 +15,7 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-type document_request =
-  uri:string -> doc:Fleche.Doc.t -> (Yojson.Safe.t, int * string) Result.t
-
+type document_request = uri:string -> doc:Fleche.Doc.t -> Yojson.Safe.t
 type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t
 
 val symbols : document_request