From cb5b6880e3277ec4e7dfa09870c7c921769e1f64 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 26 Dec 2022 01:23:22 +0100
Subject: [PATCH] [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               |  8 ++++----
 controller/coq_lsp.ml    | 14 +++++++++++---
 editor/code/package.json |  5 +++++
 fleche/config.ml         |  3 +++
 4 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 6323d2cfa..266e618d4 100644
--- a/CHANGES.md
+++ b/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
 -----------------------
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 52f85e258..0c4b9cadd 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -434,13 +434,21 @@ 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 )
 
diff --git a/editor/code/package.json b/editor/code/package.json
index eed1727ba..77080cc5d 100644
--- a/editor/code/package.json
+++ b/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."
           }
         }
       }
diff --git a/fleche/config.ml b/fleche/config.ml
index 7b2db85ff..20cdb85d7 100644
--- a/fleche/config.ml
+++ b/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