aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/pp.mli60
-rw-r--r--plugins/omega/coq_omega.ml2
-rw-r--r--plugins/romega/refl_omega.ml20
-rw-r--r--plugins/xml/cic2acic.ml11
-rw-r--r--plugins/xml/doubleTypeInference.ml4
-rw-r--r--plugins/xml/proofTree2Xml.ml422
-rw-r--r--pretyping/classops.ml2
-rw-r--r--proofs/tactic_debug.ml2
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/autorewrite.mli2
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/mltop.ml46
-rw-r--r--toplevel/mltop.mli5
-rw-r--r--toplevel/obligations.ml6
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/vernacentries.ml22
17 files changed, 68 insertions, 104 deletions
diff --git a/lib/pp.mli b/lib/pp.mli
index 8b3f6ff24..e3a3535e9 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -74,38 +74,6 @@ val tb : unit -> std_ppcmds
val close : unit -> std_ppcmds
val tclose : unit -> std_ppcmds
-(** {6 Pretty-printing functions {% \emph{%}without flush{% }%}. } *)
-
-val pp_with : Format.formatter -> std_ppcmds -> unit
-val ppnl_with : Format.formatter -> std_ppcmds -> unit
-val warning_with : Format.formatter -> string -> unit
-val warn_with : Format.formatter -> std_ppcmds -> unit
-val pp_flush_with : Format.formatter -> unit -> unit
-
-val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
-
-(** {6 Pretty-printing functions {% \emph{%}with flush{% }%}. } *)
-
-val msg_with : Format.formatter -> std_ppcmds -> unit
-val msgnl_with : Format.formatter -> std_ppcmds -> unit
-
-
-(** {6 ... } *)
-(** The following functions are instances of the previous ones on
- [std_ft] and [err_ft]. *)
-
-(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
-
-(** These functions are low-level interace to printing and should not be used
- in usual code. Consider using the [msg_*] function family instead. *)
-
-val pp : std_ppcmds -> unit
-val ppnl : std_ppcmds -> unit
-val pperr : std_ppcmds -> unit
-val pperrnl : std_ppcmds -> unit
-val pp_flush : unit -> unit
-val flush_all: unit -> unit
-
(** {6 Sending messages to the user } *)
val msg_info : std_ppcmds -> unit
@@ -164,3 +132,31 @@ val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val surround : std_ppcmds -> std_ppcmds
+
+(** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *)
+
+val pp_with : Format.formatter -> std_ppcmds -> unit
+val ppnl_with : Format.formatter -> std_ppcmds -> unit
+val warning_with : Format.formatter -> string -> unit
+val warn_with : Format.formatter -> std_ppcmds -> unit
+val pp_flush_with : Format.formatter -> unit -> unit
+
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
+
+(** These functions are low-level interface to printing and should not be used
+ in usual code. Consider using the [msg_*] function family instead. *)
+
+val pp : std_ppcmds -> unit
+val ppnl : std_ppcmds -> unit
+val pperr : std_ppcmds -> unit
+val pperrnl : std_ppcmds -> unit
+val pp_flush : unit -> unit
+val flush_all: unit -> unit
+
+val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
+
+(** {6 Low-level pretty-printing functions {% \emph{%}with flush{% }%}. } *)
+
+val msg_with : Format.formatter -> std_ppcmds -> unit
+val msgnl_with : Format.formatter -> std_ppcmds -> unit
+
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ddaf82a18..2a98cae53 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -509,7 +509,6 @@ let context operation path (t : constr) =
| ((P_TYPE :: p), LetIn (n,b,t,c)) ->
(mkLetIn (n,b,loop i p t,c))
| (p, _) ->
- ppnl (Printer.pr_lconstr t);
failwith ("abstract_path " ^ string_of_int(List.length p))
in
loop 1 path t
@@ -530,7 +529,6 @@ let occurence path (t : constr) =
| ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
| ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
| (p, _) ->
- ppnl (Printer.pr_lconstr t);
failwith ("occurence " ^ string_of_int(List.length p))
in
loop path t
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 550a4af2b..931ce400e 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -6,6 +6,7 @@
*************************************************************************)
+open Pp
open Errors
open Util
open Const_omega
@@ -17,7 +18,7 @@ open OmegaSolver
let debug = ref false
let show_goal gl =
- if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl
+ if !debug then (); Tacticals.tclIDTAC gl
let pp i = print_int i; print_newline (); flush stdout
@@ -160,16 +161,15 @@ let indice = function Left x | Right x -> x
(* Affichage de l'environnement de réification (termes et propositions) *)
let print_env_reification env =
let rec loop c i = function
- [] -> Printf.printf " ===============================\n\n"
+ [] -> str " ===============================\n\n"
| t :: l ->
- Printf.printf " (%c%02d) := " c i;
- Pp.ppnl (Printer.pr_lconstr t);
- Pp.flush_all ();
- loop c (succ i) l in
- print_newline ();
- Printf.printf " ENVIRONMENT OF PROPOSITIONS :\n\n"; loop 'P' 0 env.props;
- Printf.printf " ENVIRONMENT OF TERMS :\n\n"; loop 'V' 0 env.terms
-
+ let s = Printf.sprintf "(%c%02d)" c i in
+ spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++
+ loop c (succ i) l
+ in
+ let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
+ let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in
+ msg_debug (prop_info ++ fnl () ++ term_info)
(* \subsection{Gestion des environnements de variable pour Omega} *)
(* generation d'identifiant d'equation pour Omega *)
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index e29fcd0e8..62f7cc7cf 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -351,7 +351,7 @@ try
Acic.CicHash.find terms_to_types tt
with _ ->
(*CSC: Warning: it really happens, for example in Ring_theory!!! *)
-Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
+Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
else
(* We are already in an inner-type and Coscoy's double *)
(* type inference algorithm has not been applied. *)
@@ -363,15 +363,6 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
(Termops.refresh_universes tt)) ;
D.expected = None}
in
-(* Debugging only:
-print_endline "TERMINE:" ; flush stdout ;
-Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ;
-print_endline "TIPO:" ; flush stdout ;
-Pp.ppnl (Printer.pr_lconstr synthesized) ; flush stdout ;
-print_endline "ENVIRONMENT:" ; flush stdout ;
-Pp.ppnl (Printer.pr_context_of env) ; flush stdout ;
-print_endline "FINE_ENVIRONMENT" ; flush stdout ;
-*)
let innersort =
let synthesized_innersort =
get_sort_family_of env evar_map synthesized
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 24a383250..b1838f4a4 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -147,7 +147,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
(try
Typeops.judge_of_type u
with _ -> (* Successor of a non universe-variable universe anomaly *)
- (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;
+ Pp.msg_warning (Pp.str "Universe refresh performed!!!");
Typeops.judge_of_type (Termops.new_univ ())
)
@@ -239,7 +239,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
in
(*CSC: debugging stuff to be removed *)
if Acic.CicHash.mem subterms_to_types cstr then
- (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)) ; flush stdout ) ;
+ Pp.msg_warning (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr));
Acic.CicHash.add subterms_to_types cstr types ;
E.make_judge cstr res
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index a45b8cda4..033e83410 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -56,16 +56,6 @@ let constr_to_xml obj sigma env =
Errors.anomaly
("Problem during the conversion of constr into XML: " ^
Printexc.to_string e)
-(* CSC: debugging stuff
-Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ;
-Pp.ppnl (Pp.str "ENVIRONMENT:") ;
-Pp.ppnl (Printer.pr_context_of rel_env) ;
-Pp.ppnl (Pp.str "TERM:") ;
-Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ;
-Pp.ppnl (Pp.str "RAW-TERM:") ;
-Pp.ppnl (Printer.pr_lconstr obj') ;
-Xml.xml_empty "MISSING TERM" [] (*; raise e*)
-*)
;;
let first_word s =
@@ -98,20 +88,10 @@ let
let module X = Xml in
let ids_of_node node =
let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in
-(*
-let constr =
- try
- Proof2aproof.ProofTreeHash.find proof_tree_to_constr node
- with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated
-no lambda-term: ") (Refiner.print_script true (Evd.empty)
-(Global.named_context ()) node)) ; assert false (* Closed bug, should not
-happen any more *)
-in
-*)
try
Some (Acic.CicHash.find constr_to_ids constr)
with _ ->
-Pp.ppnl (Pp.(++) (Pp.str
+Pp.msg_warning (Pp.(++) (Pp.str
"The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
(Printer.pr_lconstr constr)) ;
None
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index cc664f9b5..87740d618 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -324,7 +324,7 @@ let add_coercion_in_graph (ic,source,target) =
old_inheritance_graph
end;
if (!ambig_paths <> []) && is_verbose () then
- ppnl (message_ambig !ambig_paths)
+ msg_warning (message_ambig !ambig_paths)
type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 916bced9e..6a0496300 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -145,7 +145,7 @@ let debug_prompt lev g tac f =
with e ->
skip:=0; skipped:=0;
if Logic.catchable_exception e then
- ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
+ msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
raise e
(* Prints a constr *)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4981e7033..e9a852455 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -91,7 +91,7 @@ let find_matches bas pat =
List.map (fun ((_,rew), esubst, subst) -> rew) res
let print_rewrite_hintdb bas =
- ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++
+ (str "Database " ++ str bas ++ (Pp.cut ()) ++
prlist_with_sep Pp.cut
(fun h ->
str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index a3fc72959..e5ec949ed 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -39,7 +39,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> tac
val auto_multi_rewrite_with : ?conds:conditions -> tactic -> string list -> Locus.clause -> tactic
-val print_rewrite_hintdb : string -> unit
+val print_rewrite_hintdb : string -> Pp.std_ppcmds
open Clenv
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a628fe26a..336c451d0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2775,7 +2775,7 @@ let subst_global_reference subst =
let subst_global ref =
let ref',t' = subst_global subst ref in
if not (eq_constr (constr_of_global ref') t') then
- ppnl (str "Warning: The reference " ++ pr_global ref ++ str " is not " ++
+ msg_warning (str "The reference " ++ pr_global ref ++ str " is not " ++
str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
pr_global ref') ;
ref'
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 12ce73a5b..2f5ed1181 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -380,7 +380,7 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
constrimpls)
impls;
- if_verbose ppnl (minductive_message names);
+ if_verbose msg_info (minductive_message names);
declare_default_schemes mind;
mind
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4f55cb896..176c0577e 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -324,11 +324,11 @@ let declare_ml_modules local l =
let print_ml_path () =
let l = !coq_mlpath_copy in
- ppnl (str"ML Load Path:" ++ fnl () ++ str" " ++
- hv 0 (prlist_with_sep fnl str l))
+ str"ML Load Path:" ++ fnl () ++ str" " ++
+ hv 0 (prlist_with_sep fnl str l)
(* Printing of loaded ML modules *)
let print_ml_modules () =
let l = get_loaded_modules () in
- pp (str"Loaded ML Modules: " ++ pr_vertical_list str l)
+ str"Loaded ML Modules: " ++ pr_vertical_list str l
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 99b96ed7b..66fbbbded 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -74,6 +74,5 @@ type ml_module_object = {
val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
-val print_ml_path : unit -> unit
-
-val print_ml_modules : unit -> unit
+val print_ml_path : unit -> Pp.std_ppcmds
+val print_ml_modules : unit -> Pp.std_ppcmds
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index aa6fbffe4..1b420407c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -916,16 +916,16 @@ let show_term n =
let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
- Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
+ let info = str (string_of_id n) ++ str " has type-checked" in
let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Array.length obls = 0 then (
- Flags.if_verbose ppnl (str ".");
+ Flags.if_verbose msg_info (info ++ str ".");
let cst = declare_definition prg in
Defined cst)
else (
let len = Array.length obls in
- let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
+ let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
progmap_add n prg;
let res = auto_solve_obligations (Some n) tactic in
match res with
diff --git a/toplevel/record.ml b/toplevel/record.ml
index a81dfa135..f9a3d2c12 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -123,7 +123,7 @@ let warning_or_error coe indsp err =
(pr_id fi ++ strbrk " cannot be defined because it is not typable.")
in
if coe then errorlabstrm "structure" st;
- Flags.if_verbose ppnl (hov 0 (str"Warning: " ++ st))
+ Flags.if_verbose msg_warning (hov 0 (str"Warning: " ++ st))
type field_status =
| NoProjection of name
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 282e2d051..485b46aef 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1233,20 +1233,20 @@ let vernac_print = function
| PrintModules -> msg_info (print_modules ())
| PrintModule qid -> print_module qid
| PrintModuleType qid -> print_modtype qid
- | PrintMLLoadPath -> Mltop.print_ml_path ()
- | PrintMLModules -> Mltop.print_ml_modules ()
+ | PrintMLLoadPath -> msg_info (Mltop.print_ml_path ())
+ | PrintMLModules -> msg_info (Mltop.print_ml_modules ())
| PrintName qid ->
if !pcoq <> None then (Option.get !pcoq).print_name qid
else msg_info (print_name qid)
- | PrintGraph -> ppnl (Prettyp.print_graph())
- | PrintClasses -> ppnl (Prettyp.print_classes())
- | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses())
- | PrintInstances c -> ppnl (Prettyp.print_instances (smart_global c))
- | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
- | PrintCoercions -> ppnl (Prettyp.print_coercions())
+ | PrintGraph -> msg_info (Prettyp.print_graph())
+ | PrintClasses -> msg_info (Prettyp.print_classes())
+ | PrintTypeClasses -> msg_info (Prettyp.print_typeclasses())
+ | PrintInstances c -> msg_info (Prettyp.print_instances (smart_global c))
+ | PrintLtac qid -> msg_info (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
+ | PrintCoercions -> msg_info (Prettyp.print_coercions())
| PrintCoercionPaths (cls,clt) ->
- ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
- | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ())
+ msg_info (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
+ | PrintCanonicalConversions -> msg_info (Prettyp.print_canonical_projections ())
| PrintUniverses (b, None) ->
let univ = Global.universes () in
let univ = if b then Univ.sort_universes univ else univ in
@@ -1255,7 +1255,7 @@ let vernac_print = function
| PrintHint r -> msg_info (Auto.pr_hint_ref (smart_global r))
| PrintHintGoal -> msg_info (Auto.pr_applicable_hint ())
| PrintHintDbName s -> msg_info (Auto.pr_hint_db_by_name s)
- | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
+ | PrintRewriteHintDbName s -> msg_info (Autorewrite.print_rewrite_hintdb s)
| PrintHintDb -> msg_info (Auto.pr_searchtable ())
| PrintScopes ->
pp (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 10:17:18 +0000