From 2198b7ca02fc7f40cda74bf9fe701adec93984e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 4 Jun 2024 02:21:41 +0200
Subject: [PATCH] [fleche] Preserve view hint across document changes.

This way we get continuous checking mode when the view-port heuristic
is enabled.
---
 CHANGES.md       |  3 +++
 fleche/theory.ml | 22 ++++++++++++----------
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index b4bb537c5..c2c8855a7 100644
--- a/CHANGES.md
+++ b/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_...
 ----------------------------------------------------
diff --git a/fleche/theory.ml b/fleche/theory.ml
index d176e054b..761b7f3eb 100644
--- a/fleche/theory.ml
+++ b/fleche/theory.ml
@@ -214,17 +214,19 @@ 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 *)
@@ -232,7 +234,7 @@ end = struct
     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 =