From 6aa145631b595a72dd613981d4ac2aa405ef06a0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 28 Jun 2023 16:38:23 +0200
Subject: [PATCH] [protocol] Rework verbosity into more granular options.

---
 CHANGES.md            |  2 ++
 controller/coq_lsp.ml |  2 ++
 fleche/config.ml      | 13 +++++++++++--
 fleche/theory.ml      |  4 ++--
 4 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 687fc20a..ae70ba65 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -37,6 +37,8 @@
  - Be more resilient when serializing unknowns Asts (@ejgallego, #503,
    reported by Gijs Pennings)
  - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, #511)
+ - More granular options `send_perf_data` `send_diags`, `verbosity`
+   will set them now (@ejgallego, #)
 
 # coq-lsp 0.1.6: Peek
 ---------------------
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index eff4cae4..1b6bbbb7 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -136,6 +136,8 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
     let workspaces = lsp_init_loop ~ifn ~ofn ~cmdline ~debug in
     let io =
       if !Fleche.Config.v.verbosity < 2 then (
+        Fleche.Config.(
+          v := { !v with send_diags = false; send_perf_data = false });
         LIO.set_log_fn (fun _obj -> ());
         let io = concise_cb ofn in
         Fleche.Io.CallBack.set io;
diff --git a/fleche/config.ml b/fleche/config.ml
index e85f3afb..73fffc6d 100644
--- a/fleche/config.ml
+++ b/fleche/config.ml
@@ -36,9 +36,16 @@ type t =
   ; pp_type : int [@default 0]
         (** Pretty-printing type in Info Panel Request, 0 = string; 1 = Pp.t; 2
             = Coq Layout Engine *)
-  ; show_stats_on_hover : bool [@default false]
-  ; verbosity : int [@default 2]
+  ; show_stats_on_hover : bool [@default false]  (** Show stats on hover *)
   ; pp_json : bool [@default false]
+        (** Whether to pretty print the protocol JSON on the wire *)
+  ; send_perf_data : bool [@default true]
+        (** Whether to send the perf data notification *)
+  ; send_diags : bool [@default true]
+        (** Whether to send the diagnostics notification *)
+  ; verbosity : int [@default 2]
+        (** Verbosity, 1 = reduced, 2 = default. As of today reduced will
+            disable all logging, and the diagnostics and perf_data notification *)
   }
 
 let default =
@@ -57,6 +64,8 @@ let default =
   ; show_stats_on_hover = false
   ; verbosity = 2
   ; pp_json = false
+  ; send_perf_data = true
+  ; send_diags = true
   }
 
 let v = ref default
diff --git a/fleche/theory.ml b/fleche/theory.ml
index 7e2c0f81..c2ab2163 100644
--- a/fleche/theory.ml
+++ b/fleche/theory.ml
@@ -137,7 +137,7 @@ let diags_of_doc doc = List.concat_map Doc.Node.diags doc.Doc.nodes
 
 let send_diags ~io ~doc =
   let diags = diags_of_doc doc in
-  if List.length diags > 0 || !Config.v.verbosity > 1 then
+  if List.length diags > 0 || !Config.v.send_diags then
     let uri, version = (doc.uri, doc.version) in
     Io.Report.diagnostics ~io ~uri ~version diags
 
@@ -173,7 +173,7 @@ end = struct
       let doc = Doc.check ~io ~target ~doc:handle.doc () in
       let requests = Handle.update_doc_info ~handle ~doc in
       send_diags ~io ~doc;
-      if !Config.v.verbosity > 1 then
+      if !Config.v.send_perf_data then
         if (* Only if completed! *)
            completed ~doc then send_perf_data ~io ~doc;
       (* Only if completed! *)