From c8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Oct 2015 11:40:22 +0200 Subject: Miscellaneous typos, spacing, US spelling in comments or variable names. --- proofs/logic_monad.ml | 2 +- proofs/proof_global.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index 81f02b66db..b9165aa812 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -188,7 +188,7 @@ struct shape of the monadic type is reminiscent of that of the continuation monad transformer. - The paper also contains the rational for the [split] abstraction. + The paper also contains the rationale for the [split] abstraction. An explanation of how to derive such a monad from mathematical principles can be found in "Kan Extensions for Program diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 028116049c..fcb706cc8d 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -94,7 +94,7 @@ val start_dependent_proof : val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. - * Both access the current proof state. The formes is supposed to be + * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context -- cgit v1.2.3 From 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 19 Oct 2015 18:12:27 +0200 Subject: Categorizing debug messages as such + NonLogical uses loggers. --- proofs/logic_monad.ml | 15 +++++++-------- proofs/logic_monad.mli | 9 +++++---- proofs/tactic_debug.ml | 6 +++--- 3 files changed, 15 insertions(+), 15 deletions(-) (limited to 'proofs') 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 -- cgit v1.2.3