From afe19aba7f12c4251f7fa8e99580739b57ab1276 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 22 Dec 2022 22:40:41 +0100
Subject: [PATCH] [fleche] Resume checking from common prefix on new version.

This does greatly reduce latency when editing deep down in a
document; closes #110 .

Also, kind of makes the need for parsing caching (#25, #36) moot, at
least with the current checking workflow.
---
 CHANGES.md    |  5 +++--
 fleche/doc.ml | 30 ++++++++++++++++++++++++++----
 2 files changed, 29 insertions(+), 6 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 389d5fa05..3d1f01787 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,8 +1,8 @@
 # coq-lsp 0.1.1: Location
 -------------------------
 
- - Don't crash if the log file can't be created (@ejgallego , #87)
- - Use LSP functions for client-side logging (@ejgallego , #87)
+ - Don't crash if the log file can't be created (@ejgallego, #87)
+ - Use LSP functions for client-side logging (@ejgallego, #87)
  - Log `_CoqProject` detection settings to client window (@ejgallego, #88)
  - Use plugin include paths from `_CoqProject` (@ejgallego, #88)
  - Support OCaml >= 4.12 (@ejgallego, #93)
@@ -16,6 +16,7 @@
  - Send `$/coq/fileProgress` progress notifications from server,
    similarly to what Lean does; display them in Code's right gutter
    (@ejgallego, #106, fixes #54)
+ - Resume checking from common prefix on document update (@ejgallego, #111)
 
 # coq-lsp 0.1.0: Memory
 -----------------------
diff --git a/fleche/doc.ml b/fleche/doc.ml
index 5c9124fe1..a3f4fd129 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -66,16 +66,38 @@ let create ~state ~workspace ~uri ~version ~contents =
   ; completed = Stopped (init_loc ~uri)
   }
 
+let recover_up_to_offset doc offset =
+  Io.Log.error "prefix" (Format.asprintf "common prefix offset found at %d" offset);
+  (* let rec find acc_nodes acc_diags nodes diags loc = *)
+  (*   if  *)
+  [], (init_loc ~uri:doc.uri)
+
+let compute_common_prefix ~contents doc =
+  let s1 = doc.contents in
+  let l1 = String.length s1 in
+  let s2 = contents in
+  let l2 = String.length s2 in
+  let rec match_or_stop i =
+    if i = l1 || i = l2 then i
+    else if Char.equal s1.[i] s2.[i] then match_or_stop (i + 1)
+    else i
+  in
+  let common_idx = match_or_stop 0 in
+  let nodes, loc = recover_up_to_offset doc common_idx in
+  let completed = Completion.Stopped loc in
+  (nodes, completed)
+
 let bump_version ~version ~contents doc =
+  (* When a new document, we resume checking from a common prefix *)
+  let nodes, completed = compute_common_prefix ~contents doc in
   let end_loc = get_last_text contents in
-  (* We need to resume checking in full when a new document *)
   { doc with
     version
-  ; nodes = []
+  ; nodes
   ; contents
   ; end_loc
-  ; diags_dirty = false
-  ; completed = Stopped (init_loc ~uri:doc.uri)
+  ; diags_dirty = true          (* EJGA: Is it worth to optimize this? *)
+  ; completed
   }
 
 let add_node ~node doc =