diff options
| -rw-r--r-- | proofs/logic_monad.ml | 15 | ||||
| -rw-r--r-- | proofs/logic_monad.mli | 9 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
4 files changed, 18 insertions, 18 deletions
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index b9165aa812..e3caa886a2 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -94,14 +94,6 @@ struct let print_char = fun c -> (); fun () -> print_char c - (** {!Pp.pp}. The buffer is also flushed. *) - 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 () -> Control.timeout n t (Exception Timeout) @@ -111,6 +103,13 @@ struct let (e, info) = Errors.push e in Util.iraise (Exception e, info) + (** Use the current logger. The buffer is also flushed. *) + let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) + let print_info s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) + let print_warning s = make (fun _ -> Pp.msg_warning s;Pp.pp_flush ()) + let print_error s = make (fun _ -> Pp.msg_error s;Pp.pp_flush ()) + let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ()) + let run = fun x -> try x () with Exception e as src -> let (src, info) = Errors.push src in diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli index 511dd7a6ed..84ffda7533 100644 --- a/proofs/logic_monad.mli +++ b/proofs/logic_monad.mli @@ -55,12 +55,13 @@ module NonLogical : sig val read_line : string t val print_char : char -> unit t - (** {!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. *) + (** Loggers. The buffer is also flushed. *) val print_debug : Pp.std_ppcmds -> unit t + val print_warning : Pp.std_ppcmds -> unit t + val print_notice : Pp.std_ppcmds -> unit t + val print_info : Pp.std_ppcmds -> unit t + val print_error : Pp.std_ppcmds -> unit t (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 667765dbf2..6d6215c521 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -33,7 +33,7 @@ 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_debug (s++fnl()) -let msg_tac_notice s = Proofview.NonLogical.print (s++fnl()) +let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) (* Prints the goal *) @@ -122,7 +122,7 @@ let run ini = let open Proofview.NonLogical in if not ini then begin - Proofview.NonLogical.print (str"\b\r\b\r") >> + Proofview.NonLogical.print_notice (str"\b\r\b\r") >> !skipped >>= fun skipped -> msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl()) end >> @@ -137,7 +137,7 @@ let rec prompt level = let runtrue = run true in begin let open Proofview.NonLogical in - Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> + Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 96d0b592b8..5a0d26a1cb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,8 +44,8 @@ open Proofview.Notations let safe_msgnl s = Proofview.NonLogical.catch - (Proofview.NonLogical.print (s++fnl())) - (fun _ -> Proofview.NonLogical.print (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) + (Proofview.NonLogical.print_debug (s++fnl())) + (fun _ -> Proofview.NonLogical.print_warning (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) type value = tlevel generic_argument @@ -1136,7 +1136,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with interp_message ist s >>= fun msg -> return (hov 0 msg , hov 0 msg) in - let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in + let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print_info msgnl)) in let log (msg,_) = Proofview.Trace.log (fun () -> msg) in let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in Ftactic.run msgnl begin fun msgnl -> |