Fixing emacs output in debugging mode.

Goal displaying during Debugging ltac is a notice message now. Other
messages are debug messages. This does not change anything in coqide
or coqtop, but allows proofgeneral to dispatch them in the right
buffers (pg had to be fixed too).

3 files changed, 12 insertions, 3 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index cb3e5a1860..81f02b66db 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -95,7 +95,11 @@ struct
   let print_char = fun c -> (); fun () -> print_char c
 
   (** {!Pp.pp}. The buffer is also flushed. *)
-  let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
+  let print_debug = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
+    let (e, info) = Errors.push e in raise ~info e ()
+
+  (** {!Pp.pp}. The buffer is also flushed. *)
+  let print = fun s -> (); fun () -> try Pp.msg_notice s; Pp.pp_flush () with e ->
     let (e, info) = Errors.push e in raise ~info e ()
 
   let timeout = fun n t -> (); fun () ->
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index ab729aff71..511dd7a6ed 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -58,6 +58,10 @@ module NonLogical : sig
   (** {!Pp.pp}. The buffer is also flushed. *)
   val print : Pp.std_ppcmds -> unit t
 
+  (* FIXME: shouldn't we have a logger instead? *)
+  (** {!Pp.pp}. The buffer is also flushed. *)
+  val print_debug : Pp.std_ppcmds -> unit t
+
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
   val raise : ?info:Exninfo.info -> exn -> 'a t
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index d7f4b5ead5..667765dbf2 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -32,7 +32,8 @@ let explain_logic_error = ref (fun e -> mt())
 
 let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
-let msg_tac_debug s = Proofview.NonLogical.print (s++fnl())
+let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
+let msg_tac_notice s = Proofview.NonLogical.print (s++fnl())
 
 (* Prints the goal *)
 
@@ -48,7 +49,7 @@ let db_pr_goal gl =
 let db_pr_goal =
   Proofview.Goal.nf_enter begin fun gl ->
   let pg = db_pr_goal gl in
-  Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
+  Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
   end