[feedback] Remove unused tag on `Debug` level.

IMO level indicators are not the proper place to store this information.

5 files changed, 12 insertions, 12 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 61f002576b..11621078de 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -298,7 +298,7 @@ let handle_intermediate_message handle level content =
         | Feedback.Info    -> fun s -> Minilib.log ~level:`INFO    (xml_to_string s)
         | Feedback.Notice  -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
         | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
-        | Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
+        | Feedback.Debug   -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
   in
   logger level content
 
@@ -333,7 +333,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
     state.fragment <- String.sub s l_end (String.length s - l_end);
     state.lexerror <- None;
     match Xmlprotocol.is_message xml with
-    | Some (lvl, msg) ->
+    | Some (lvl, _loc, msg) ->
       handle_intermediate_message handle lvl msg;
       loop ()
     | None ->
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 00c3f88e56..f0698a54a3 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -301,7 +301,7 @@ type logger = Feedback.level -> Richpp.richpp -> unit
 
 let default_logger level message =
   let level = match level with
-  | Feedback.Debug _ -> `DEBUG
+  | Feedback.Debug -> `DEBUG
   | Feedback.Info -> `INFO
   | Feedback.Notice -> `NOTICE
   | Feedback.Warning -> `WARNING
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index a55d19aa1b..65c85ed153 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -769,15 +769,15 @@ let document to_string_fmt =
 open Feedback
 
 let of_message_level = function
-  | Debug s ->
-      Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
+  | Debug ->
+      Serialize.constructor "message_level" "debug" []
   | Info -> Serialize.constructor "message_level" "info" []
   | Notice -> Serialize.constructor "message_level" "notice" []
   | Warning -> Serialize.constructor "message_level" "warning" []
   | Error -> Serialize.constructor "message_level" "error" []
 let to_message_level =
   Serialize.do_match "message_level" (fun s args -> match s with
-  | "debug" -> Debug (Serialize.raw_string args)
+  | "debug" -> Debug
   | "info" -> Info
   | "notice" -> Notice
   | "warning" -> Warning
diff --git a/lib/feedback.ml b/lib/feedback.ml
index d6f580fd16..74a18df6f8 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -9,7 +9,7 @@
 open Xml_datatype
 
 type level =
-  | Debug of string
+  | Debug
   | Info
   | Notice
   | Warning
@@ -85,7 +85,7 @@ let make_body quoter info s = quoter (hov 0 (info ++ s))
 
 (* Generic logger *)
 let gen_logger dbg err level msg = match level with
-  | Debug _ -> msgnl (make_body dbg  dbg_str msg)
+  | Debug   -> msgnl (make_body dbg  dbg_str msg)
   | Info    -> msgnl (make_body dbg info_str msg)
   | Notice  -> msgnl msg
   | Warning -> Flags.if_warn (fun () ->
@@ -99,7 +99,7 @@ let std_logger   = gen_logger (fun x -> x) (fun x -> x)
 let color_terminal_logger level strm =
   let msg = Ppstyle.color_msg in
   match level with
-  | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
+  | Debug   -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
   | Info    -> msg !std_ft strm
   | Notice  -> msg !std_ft strm
   | Warning ->
@@ -121,7 +121,7 @@ let msg_info    x = !logger Info x
 let msg_notice  x = !logger Notice x
 let msg_warning x = !logger Warning x
 let msg_error   x = !logger Error x
-let msg_debug   x = !logger (Debug "_") x
+let msg_debug   x = !logger Debug x
 
 (** Feeders *)
 let feeder = ref ignore
@@ -148,7 +148,7 @@ let feedback_logger lvl msg =
 let ft_logger old_logger ft level mesg =
   let id x = x in
   match level with
-  | Debug _ -> msgnl_with ft (make_body id  dbg_str mesg)
+  | Debug   -> msgnl_with ft (make_body id  dbg_str mesg)
   | Info    -> msgnl_with ft (make_body id info_str mesg)
   | Notice  -> msgnl_with ft mesg
   | Warning -> old_logger level mesg
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 50ffd22db9..690877897e 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -10,7 +10,7 @@ open Xml_datatype
 
 (* Old plain messages (used to be in Pp) *)
 type level =
-  | Debug of string
+  | Debug
   | Info
   | Notice
   | Warning