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 =