[fleche] Preserve view hint across document changes.

This way we get continuous checking mode when the view-port heuristic
is enabled.

CHANGES.md

@@ -4,6 +4,9 @@
 - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
   dependency, and will greatly easy the development of tools that
   require AST manipulation (@ejgallego, #698)
+- [fleche] Preserve view hint across document changes. We get local
+  continuous checking mode when the view-port heuristic is enabled
+  (@ejgallego, #)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

fleche/theory.ml

@@ -214,25 +214,27 @@ end = struct
       | None -> pend_try f tt
       | Some r -> Some r)
 
-  let hint : (int * int) option ref = ref None
+  let hint : (Lang.LUri.File.t * (int * int)) option ref = ref None
 
-  let get_check_target pt_requests =
+  let get_check_target ~(doc : Doc.t) pt_requests =
     let target_of_pt_handle (_, (l, c)) = Doc.Target.Position (l, c) in
     match Option.map target_of_pt_handle (List.nth_opt pt_requests 0) with
     | None ->
-      Option.map
-        (fun (l, c) ->
-          hint := None;
-          Doc.Target.Position (l, c))
-        !hint
+      Option.bind !hint (fun (uri, (l, c)) ->
+          if Lang.LUri.File.equal uri doc.uri then
+            match doc.completed with
+            | Yes _ | Failed _ | FailedPermanent _ -> None
+            | Stopped range when Doc.Target.reached ~range (l, c) -> None
+            | Stopped _ -> Some (Doc.Target.Position (l, c))
+          else None)
     | Some t -> Some t
 
   (* Notification handling; reply is optional / asynchronous *)
   let check ~io ~token ~uri =
     Io.Log.trace "process_queue" "resuming document checking";
     match Handle.find_opt ~uri with
     | Some handle -> (
-      let target = get_check_target handle.pt_requests in
+      let target = get_check_target ~doc:handle.doc handle.pt_requests in
       match target with
       (* If we are in lazy mode and we don't have any full document requests
          pending, we just deschedule *)
@@ -276,9 +278,9 @@ end = struct
 
   let set_scheduler_hint ~uri ~point =
     if CList.is_empty !pending then
-      let () = hint := Some point in
+      let () = hint := Some (uri, point) in
       schedule ~uri (* if the hint is set we wanna override it *)
-    else if not (Option.is_empty !hint) then hint := Some point
+    else if not (Option.is_empty !hint) then hint := Some (uri, point)
 end
 
 let create ~io ~token ~env ~uri ~raw ~version =