Merge pull request #517 from ejgallego/verbosity_to_options

[protocol] Rework verbosity into more granular options.

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
 ---------------------

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;

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

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! *)