diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 19:53:57 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 19:53:57 +0000 |
commit | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (patch) | |
tree | 75f2746f738c2b2c111b701f80d59d10f80c75f7 | |
parent | cf7660a3a8932ee593a376e8ec7ec251896a72e3 (diff) |
Cleaning Pp.ppnl use
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | lib/pp.mli | 60 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 2 | ||||
-rw-r--r-- | plugins/romega/refl_omega.ml | 20 | ||||
-rw-r--r-- | plugins/xml/cic2acic.ml | 11 | ||||
-rw-r--r-- | plugins/xml/doubleTypeInference.ml | 4 | ||||
-rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 22 | ||||
-rw-r--r-- | pretyping/classops.ml | 2 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 2 | ||||
-rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
-rw-r--r-- | tactics/autorewrite.mli | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
-rw-r--r-- | toplevel/command.ml | 2 | ||||
-rw-r--r-- | toplevel/mltop.ml4 | 6 | ||||
-rw-r--r-- | toplevel/mltop.mli | 5 | ||||
-rw-r--r-- | toplevel/obligations.ml | 6 | ||||
-rw-r--r-- | toplevel/record.ml | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 22 |
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)) |