[diagnostics] Don't convert Coq "Info" messages to feedbacks

We stop displaying messages such as "Foo is defined" as feedback by
default; users willing to see them can set the corresponding option.

Closes #108

CHANGES.md

@@ -1,9 +1,6 @@
-# coq-lsp 0.2.0: Location
+# coq-lsp 0.1.1: Location
 -------------------------
 
-# coq-lsp 0.1.1:
-----------------
-
  - 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)
@@ -13,6 +10,9 @@
  - Improved syntax highlighting on VSCode client (@artagnon, #105)
  - Resume document checking from the point it was interrupted
    (@ejgallego, #95, #99)
+ - Don't convert Coq "Info" messages such as "Foo is defined" to
+   feedback by default; users willing to see them can set the
+   corresponding option (@ejgallego, #113)
 
 # coq-lsp 0.1.0: Memory
 -----------------------

controller/coq_lsp.ml

@@ -434,13 +434,22 @@ let lvl_to_severity (lvl : Feedback.level) =
   | Feedback.Warning -> 2
   | Feedback.Error -> 1
 
+let add_message lvl loc msg q =
+  let lvl = lvl_to_severity lvl in
+  q := (loc, lvl, msg) :: !q
+
 let mk_fb_handler () =
   let q = ref [] in
   ( (fun Feedback.{ contents; _ } ->
       match contents with
-      | Message (lvl, loc, msg) ->
-        let lvl = lvl_to_severity lvl in
-        q := (loc, lvl, msg) :: !q
+      | Message ((Error|Warning|Notice) as lvl, loc, msg) ->
+        add_message lvl loc msg q
+      | Message (Info as lvl, loc, msg) ->
+        if (!Fleche.Config.v).show_coq_info_messages then
+          add_message lvl loc msg q
+        else ()
+      | Message (Debug, _loc, _msg) ->
+        ()
       | _ -> ())
   , q )
 

editor/code/package.json

@@ -119,6 +119,11 @@
             "type": "boolean",
             "default": false,
             "description": "When showing goals and the cursor is in a tactic, if false, show goals before executing the tactic, if true, show goals after"
+          },
+          "coq-lsp.show_coq_info_messages": {
+            "type": "boolean",
+            "default": false,
+            "description": "Show Coq's Info messages as diagnostics, such as 'foo has been defined.' and miscellaneous operational messages."
           }
         }
       }

fleche/config.ml

@@ -11,6 +11,8 @@ type t =
   ; goal_after_tactic : bool [@default false]
         (** When showing goals and the cursor is in a tactic, if false, show
             goals before executing the tactic, if true, show goals after *)
+  ; show_coq_info_messages : bool [@default false]
+        (** Ignore `msg_info` messages in diagnostics *)
   }
 
 let default =
@@ -19,6 +21,7 @@ let default =
   ; eager_diagnostics = true
   ; ok_diagnostics = false
   ; goal_after_tactic = false
+  ; show_coq_info_messages = false
   }
 
 let v = ref default