Merge pull request #104 from ejgallego/only_send_diags_when_dirty

[eager diagnostics] Only send diagnostics when they have changed

CHANGES.md

@@ -9,6 +9,7 @@
  - Log `_CoqProject` detection settings to client window (@ejgallego, #88)
  - Use plugin include paths from `_CoqProject` (@ejgallego, #88)
  - Support OCaml >= 4.12 (@ejgallego, #93)
+ - Optimize the number of diagnostics sent in eager mode (@ejgallego, #104)
 
 # coq-lsp 0.1.0: Memory
 -----------------------

fleche/doc.ml

@@ -34,6 +34,7 @@ type t =
   ; root : Coq.State.t
   ; nodes : node list
   ; diags : Types.Diagnostic.t list
+  ; diags_dirty : bool  (** Used to optimize `eager_diagnostics` *)
   ; completed : Completion.t
   }
 
@@ -51,6 +52,7 @@ let create ~state ~workspace ~uri ~version ~contents =
   ; root = mk_doc state workspace
   ; nodes = []
   ; diags = []
+  ; diags_dirty = false
   ; completed = Stopped (init_loc ~uri)
   }
 
@@ -61,11 +63,22 @@ let bump_version ~version ~text doc =
   ; nodes = []
   ; diags = []
   ; contents = text
+  ; diags_dirty = false
   ; completed = Stopped (init_loc ~uri:doc.uri)
   }
 
 let add_node ~node ~diags doc =
-  { doc with nodes = node :: doc.nodes; diags = diags @ doc.diags }
+  let diags_dirty = if diags <> [] then true else doc.diags_dirty in
+  { doc with nodes = node :: doc.nodes; diags = diags @ doc.diags; diags_dirty }
+
+let send_eager_diagnostics ~uri ~version ~doc =
+  (* this is too noisy *)
+  (* let proc_diag = mk_diag loc 3 (Pp.str "Processing") in *)
+  (* Io.Report.diagnostics ~uri ~version (proc_diag :: doc.diags)); *)
+  if doc.diags_dirty && !Config.v.eager_diagnostics then (
+    Io.Report.diagnostics ~uri ~version doc.diags;
+    { doc with diags_dirty = false })
+  else doc
 
 let set_completion ~completed doc = { doc with completed }
 
@@ -126,6 +139,11 @@ let state_recovery_heuristic st v =
     Coq.State.drop_proofs ~st
   | _ -> st
 
+let debug_parsed_sentence ~loc ~ast =
+  let line = "[l: " ^ string_of_int loc.Loc.line_nb ^ "] " in
+  Io.Log.error "coq"
+    ("parsed sentence: " ^ line ^ Pp.string_of_ppcmds (Coq.Ast.print ast))
+
 type process_action =
   | EOF of Completion.t (* completed *)
   | Skip of Loc.t (* last valid token *)
@@ -208,15 +226,8 @@ let process_and_parse ~uri ~version ~fb_queue doc loc doc_handle =
       let loc = Coq.Ast.loc ast |> Option.get in
       let last_tok_new = Pcoq.Parsable.loc doc_handle in
       (* XXX Eager update! *)
-      if !Config.v.eager_diagnostics then
-        (* this is too noisy *)
-        (* let proc_diag = mk_diag loc 3 (Pp.str "Processing") in *)
-        (* Io.Report.diagnostics ~uri ~version (proc_diag :: doc.diags)); *)
-        Io.Report.diagnostics ~uri ~version doc.diags;
-      (if Debug.parsing then
-       let line = "[l: " ^ string_of_int loc.Loc.line_nb ^ "] " in
-       Io.Log.error "coq"
-         ("parsed sentence: " ^ line ^ Pp.string_of_ppcmds (Coq.Ast.print ast)));
+      let doc = send_eager_diagnostics ~uri ~version ~doc in
+      let () = if Debug.parsing then debug_parsed_sentence ~loc ~ast in
       register_hack_proof_recover ast st;
       (* memory is disabled as it is quite slow and misleading *)
       let res, memo_info = interp_and_info ~parsing_time ~st ~fb_queue ast in

fleche/doc.mli

@@ -37,6 +37,7 @@ type t = private
   ; root : Coq.State.t
   ; nodes : node list
   ; diags : Types.Diagnostic.t list
+  ; diags_dirty : bool
   ; completed : Completion.t
   }