[fleche] Implement document scheduler

We use a simple list, LIFO strategy, which prioritizes the last event.

Fixes #563

CHANGES.md

@@ -22,6 +22,10 @@
  - Add pointers to Windows installers (@ejgallego, #559)
  - Recognize `Goal` and `Definition $id : ... .` as proof starters
    (@ejgallego, #561, reported by @Zimmi48, fixes #548)
+ - Implement a LIFO document scheduler, this is heavier in the
+   background as more documents will be checked, but provides a few
+   usability improvements (@ejgallego, #566, fixes #563, reported by
+   Ali Caglayan)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

fleche/theory.ml

@@ -175,7 +175,17 @@ module Check : sig
   val deschedule : uri:Lang.LUri.File.t -> unit
   val maybe_check : io:Io.CallBack.t -> (Int.Set.t * Doc.t) option
 end = struct
-  let pending = ref None
+  let pending = ref []
+
+  let pend_pop = function
+    | [] -> []
+    | _ :: p -> p
+
+  let pend_push uri pend = uri :: pend
+
+  let pend_bind = function
+    | [] -> fun _ -> None
+    | l :: _ -> fun f -> f l
 
   let get_check_target pt_requests =
     let target_of_pt_handle (_, (l, c)) = Doc.Target.Position (l, c) in
@@ -191,19 +201,19 @@ end = struct
       let requests = Handle.update_doc_info ~handle ~doc in
       if Doc.Completion.is_completed doc.completed then Register.fire ~io ~doc;
       (* Remove from the queu *)
-      if Doc.Completion.is_completed doc.completed then pending := None;
+      if Doc.Completion.is_completed doc.completed then
+        pending := pend_pop !pending;
       Some (requests, doc)
     | None ->
       Io.Log.trace "Check.check"
         ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
       None
 
-  let maybe_check ~io = Option.bind !pending (fun uri -> check ~io ~uri)
-  let schedule ~uri = pending := Some uri
+  let maybe_check ~io = pend_bind !pending (fun uri -> check ~io ~uri)
+  let schedule ~uri = pending := pend_push uri !pending
 
   let deschedule ~uri =
-    if Option.compare Lang.LUri.File.compare (Some uri) !pending = 0 then
-      pending := None
+    pending := CList.remove Lang.LUri.File.equal uri !pending
 end
 
 let send_error_permanent_fail ~io ~uri ~version message =
@@ -355,6 +365,7 @@ module Request = struct
           if Doc.Completion.is_completed doc.completed then Now doc
           else (
             Handle.attach_cp_request ~uri ~id;
+            Check.schedule ~uri;
             Postpone))
     | PosInDoc { uri; point; version; postpone } ->
       with_doc ~uri ~f:(fun doc ->
@@ -363,6 +374,7 @@ module Request = struct
           | true, _ -> Now doc
           | false, true ->
             Handle.attach_pt_request ~uri ~id ~point;
+            Check.schedule ~uri;
             Postpone
           | false, false -> Cancel)
 

fleche/theory.mli

@@ -63,8 +63,9 @@ module Request : sig
     | Postpone
     | Cancel
 
-  (** Add a request to be served; returns [true] if request is added to the
-      queue , [false] if the request can be already answered. *)
+  (** Add a request to be served; returns [Postpone] if request is added to the
+      queue, [Now doc] if the request is available. [Cancel] means "we will
+      never be able to serve this" *)
   val add : t -> action
 
   (** Removes the request from the list of things to wake up *)

lang/lUri.ml

@@ -23,4 +23,5 @@ module File = struct
   let extension { file; _ } = Filename.extension file
   let hash = Hashtbl.hash
   let compare = Stdlib.compare
+  let equal = Stdlib.( = )
 end

lang/lUri.mli

@@ -31,6 +31,9 @@ module File : sig
   (** compare *)
   val compare : t -> t -> int
 
+  (** equal *)
+  val equal : t -> t -> bool
+
   (** hash *)
   val hash : t -> int
 end