diff options
| -rw-r--r-- | proofs/logic_monad.ml | 6 | ||||
| -rw-r--r-- | proofs/logic_monad.mli | 4 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 5 |
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 |