From 91ee24b4a7843793a84950379277d92992ba1651 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 11 Feb 2016 02:13:30 +0100 Subject: Feedback cleanup This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work. --- _tags | 1 + checker/check.ml | 23 ++-- checker/check.mllib | 12 +- checker/check_stat.ml | 5 +- checker/checker.ml | 12 +- checker/closure.ml | 2 +- checker/indtypes.ml | 2 +- checker/mod_checking.ml | 2 +- checker/print.ml | 4 +- checker/safe_typing.ml | 4 +- dev/doc/changes.txt | 63 ++++++++++ dev/printers.mllib | 11 +- dev/top_printers.ml | 9 +- dev/vm_printers.ml | 2 +- engine/logic_monad.ml | 10 +- engine/proofview.ml | 4 +- grammar/tacextend.ml4 | 4 +- grammar/vernacextend.ml4 | 2 +- ide/coq.ml | 18 +-- ide/coqOps.ml | 17 +-- ide/coqide.ml | 2 +- ide/ide_slave.ml | 24 ++-- ide/ideutils.ml | 12 +- ide/ideutils.mli | 2 +- ide/project_file.ml4 | 14 +-- ide/wg_MessageView.ml | 6 +- interp/constrintern.ml | 2 +- interp/dumpglob.ml | 4 +- interp/implicit_quantifiers.ml | 2 +- interp/notation.ml | 8 +- interp/syntax_def.ml | 2 +- interp/topconstr.ml | 2 +- kernel/cbytegen.ml | 4 +- kernel/closure.ml | 2 +- kernel/names.ml | 2 +- kernel/nativecode.ml | 6 +- kernel/nativeconv.ml | 6 +- kernel/nativelib.ml | 16 +-- kernel/nativelibrary.ml | 10 +- kernel/reduction.ml | 2 +- kernel/term_typing.ml | 6 +- kernel/vconv.ml | 2 +- lib/aux_file.ml | 2 +- lib/clib.mllib | 5 +- lib/explore.ml | 2 +- lib/feedback.ml | 130 +++++++++++++++++++- lib/feedback.mli | 81 +++++++++++- lib/pp.ml | 164 +------------------------ lib/pp.mli | 139 +++------------------ lib/ppstyle.ml | 38 +++--- lib/ppstyle.mli | 14 +-- lib/system.ml | 14 +-- library/declare.ml | 8 +- library/goptions.ml | 15 +-- library/libobject.ml | 2 +- library/library.ml | 12 +- library/loadpath.ml | 2 +- library/nametab.ml | 6 +- ltac/extratactics.ml4 | 2 +- ltac/g_ltac.ml4 | 6 +- ltac/g_obligations.ml4 | 6 +- ltac/g_rewrite.ml4 | 2 +- ltac/tacentries.ml | 6 +- ltac/tacenv.ml | 2 +- ltac/tacinterp.ml | 2 +- ltac/tacsubst.ml | 2 +- parsing/cLexer.ml4 | 11 +- parsing/g_tactic.ml4 | 4 +- parsing/g_vernac.ml4 | 10 +- plugins/cc/ccalgo.ml | 2 +- plugins/cc/cctac.ml | 4 +- plugins/decl_mode/decl_proof_instr.ml | 6 +- plugins/extraction/extract_env.ml | 4 +- plugins/extraction/g_extraction.ml4 | 4 +- plugins/extraction/table.ml | 18 +-- plugins/firstorder/g_ground.ml4 | 4 +- plugins/firstorder/ground.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 6 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/g_indfun.ml4 | 4 +- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/indfun.ml | 8 +- plugins/funind/invfun.ml | 2 +- plugins/funind/merge.ml | 14 +-- plugins/funind/recdef.ml | 8 +- plugins/micromega/coq_micromega.ml | 22 ++-- plugins/romega/refl_omega.ml | 2 +- plugins/rtauto/proof_search.ml | 2 +- plugins/rtauto/refl_tauto.ml | 12 +- plugins/setoid_ring/g_newring.ml4 | 8 +- plugins/setoid_ring/newring.ml | 4 +- plugins/syntax/nat_syntax.ml | 2 +- pretyping/classops.ml | 2 +- pretyping/constr_matching.ml | 4 +- pretyping/detyping.ml | 2 +- pretyping/evarconv.ml | 2 +- pretyping/glob_ops.ml | 4 +- pretyping/indrec.ml | 2 +- pretyping/nativenorm.ml | 6 +- pretyping/patternops.ml | 2 +- pretyping/recordops.ml | 4 +- pretyping/reductionops.ml | 5 +- pretyping/unification.ml | 8 +- printing/printer.ml | 6 +- proofs/pfedit.ml | 2 +- proofs/proof_using.ml | 2 +- proofs/redexpr.ml | 4 +- proofs/refiner.ml | 5 +- stm/asyncTaskQueue.ml | 7 +- stm/lemmas.ml | 8 +- stm/stm.ml | 74 +++++------ tactics/auto.ml | 8 +- tactics/class_tactics.ml | 6 +- tactics/eauto.ml | 8 +- tactics/hints.ml | 4 +- tactics/tactics.ml | 4 +- tools/coqdep.ml | 4 +- tools/fake_ide.ml | 8 +- toplevel/class.ml | 4 +- toplevel/command.ml | 12 +- toplevel/coqinit.ml | 10 +- toplevel/coqloop.ml | 16 +-- toplevel/coqtop.ml | 24 ++-- toplevel/indschemes.ml | 4 +- toplevel/locality.ml | 2 +- toplevel/metasyntax.ml | 16 +-- toplevel/mltop.ml | 10 +- toplevel/obligations.ml | 18 +-- toplevel/record.ml | 4 +- toplevel/vernac.ml | 23 ++-- toplevel/vernacentries.ml | 112 ++++++++--------- toplevel/vernacinterp.ml | 4 +- 132 files changed, 813 insertions(+), 809 deletions(-) diff --git a/_tags b/_tags index f805eeaa3..e8317d614 100644 --- a/_tags +++ b/_tags @@ -67,6 +67,7 @@ "pretyping": include "printing": include "proofs": include +"stm": include "tactics": include "theories": include "tools": include diff --git a/checker/check.ml b/checker/check.ml index 3a5c91217..93eb2a0d2 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -111,15 +111,14 @@ let check_one_lib admit (dir,m) = also check if it carries a validation certificate (yet to be implemented). *) if LibrarySet.mem dir admit then - (Flags.if_verbose ppnl + (Flags.if_verbose Feedback.msg_notice (str "Admitting library: " ++ pr_dirpath dir); Safe_typing.unsafe_import file md m.library_extra_univs dig) else - (Flags.if_verbose ppnl + (Flags.if_verbose Feedback.msg_notice (str "Checking library: " ++ pr_dirpath dir); Safe_typing.import file md m.library_extra_univs dig); - Flags.if_verbose pp (fnl()); - pp_flush (); + Flags.if_verbose Feedback.msg_notice (fnl()); register_loaded_library m (*************************************************************************) @@ -173,7 +172,7 @@ let remove_load_path dir = let add_load_path (phys_path,coq_path) = if !Flags.debug then - ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ + Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); let phys_path = canonical_path_name phys_path in let physical, logical = !load_paths in @@ -188,7 +187,7 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> default_root_prefix then - msg_warning + Feedback.msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); @@ -299,7 +298,7 @@ let name_clash_message dir mdir f = let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = - Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); + Flags.if_verbose Feedback.msg_notice(str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try let ch = System.with_magic_number_check raw_intern_library f in @@ -323,7 +322,7 @@ let intern_from_file (dir, f) = errorlabstrm "intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin - pp (str " (was a vio file) "); + Feedback.msg_notice(str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then errorlabstrm "intern_from_file" (str "The file "++str f++str " is still a .vio")) @@ -334,12 +333,12 @@ let intern_from_file (dir, f) = Validate.validate !Flags.debug Values.v_libsum sd; Validate.validate !Flags.debug Values.v_lib md; Validate.validate !Flags.debug Values.v_opaques table; - Flags.if_verbose ppnl (str" done]"); pp_flush (); + Flags.if_verbose Feedback.msg_notice (str" done]"); let digest = if opaque_csts <> None then Cic.Dviovo (digest,udg) else (Cic.Dvo digest) in sd,md,table,opaque_csts,digest - with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in + with e -> Flags.if_verbose Feedback.msg_notice (str" failed!]"); raise e in depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; opaque_tables := LibraryMap.add sd.md_name table !opaque_tables; Option.iter (fun (opaque_csts,_,_) -> @@ -407,11 +406,11 @@ let recheck_library ~norec ~admit ~check = let nochk = List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in (* *) - Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ + Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ prlist (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); List.iter (check_one_lib nochk) needed; - Flags.if_verbose ppnl (str"Modules were successfully checked") + Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked") open Printf diff --git a/checker/check.mllib b/checker/check.mllib index 900cfe0c8..a093fd959 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -22,16 +22,18 @@ CList CString Serialize Stateid -Feedback -Pp -Segmenttree -Unicodetable -Unicode CObj CArray CStack Util +Pp Ppstyle +Xml_datatype +Richpp +Feedback +Segmenttree +Unicodetable +Unicode Errors CEphemeron Future diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 84f5684d4..a26c93a30 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -57,12 +57,13 @@ let print_context env = env_modules=mods; env_modtypes=mtys}; env_stratification= {env_universes=univ; env_engagement=engt}} = env in - ppnl(hov 0 + Feedback.msg_notice + (hov 0 (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_ax csts) ++ - fnl())); pp_flush() + fnl())); end let stats () = diff --git a/checker/checker.ml b/checker/checker.ml index 91a207a60..61b13c60b 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -17,7 +17,7 @@ open Check let () = at_exit flush_all let fatal_error info anomaly = - flush_all (); pperrnl info; flush_all (); + flush_all (); Feedback.msg_error info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" @@ -67,12 +67,12 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = Check.add_load_path (dir,coq_dirpath) end else - msg_warning (str "Cannot open " ++ str dir) + Feedback.msg_warning (str "Cannot open " ++ str dir) let convert_string d = try Id.of_string d with Errors.UserError _ -> - if_verbose msg_warning + if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root = List.iter Check.add_load_path dirs; Check.add_load_path (unix_path, coq_root) else - msg_warning (str "Cannot open " ++ str unix_path) + Feedback.msg_warning (str "Cannot open " ++ str unix_path) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -123,7 +123,7 @@ let init_load_path () = add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) - (xdg_dirs ~warn:(fun x -> msg_warning (str x))); + (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x))); (* then directories in COQPATH *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) @@ -288,7 +288,7 @@ let rec explain_exn = function Format.printf "@\nis not convertible with@\n"; Print.print_pure_constr a; Format.printf "@\n====== universes ====@\n"; - Pp.pp (Univ.pr_universes + Feedback.msg_notice (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" diff --git a/checker/closure.ml b/checker/closure.ml index c2708e97d..cef1d31a6 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -29,7 +29,7 @@ let reset () = beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0 let stop() = - msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ + Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]") diff --git a/checker/indtypes.ml b/checker/indtypes.ml index fd5eaeb8b..a667bb8a3 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -528,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds = (************************************************************************) let check_inductive env kn mib = - Flags.if_verbose ppnl (str " checking ind: " ++ MutInd.print kn); pp_flush (); + Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); (* check mind_constraints: should be consistent with env *) let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in (* check mind_record : TODO ? check #constructor = 1 ? *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index c07a35e35..7f93e1560 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -26,7 +26,7 @@ let refresh_arity ar = | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = - Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush (); + Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn); let env' = if cb.const_polymorphic then let inst = Univ.make_abstract_instance cb.const_universes in diff --git a/checker/print.ml b/checker/print.ml index da8a6106f..c0d1ac368 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -10,7 +10,7 @@ open Format open Cic open Names -let print_instance i = Pp.pp (Univ.Instance.pr i) +let print_instance i = Feedback.msg_notice (Univ.Instance.pr i) let print_pure_constr csr = let rec term_display c = match c with @@ -108,7 +108,7 @@ let print_pure_constr csr = and sort_display = function | Prop(Pos) -> print_string "Set" | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; Pp.pp (Univ.pr_uni u); print_string ")" + | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")" and name_display = function | Name id -> print_string (Id.to_string id) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 7f9ed92f9..1071e2f93 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -81,7 +81,7 @@ let stamp_library file digest = () warning is issued in case of mismatch *) let import file clib univs digest = let env = !genv in - check_imports msg_warning clib.comp_name env clib.comp_deps; + check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; let mb = clib.comp_mod in Mod_checking.check_module @@ -93,7 +93,7 @@ let import file clib univs digest = (* When the module is admitted, digests *must* match *) let unsafe_import file clib univs digest = let env = !genv in - if !Flags.debug then check_imports msg_warning clib.comp_name env clib.comp_deps + if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; full_add_module clib.comp_name clib.comp_mod univs digest diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2f631c633..53497ff0e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,69 @@ = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= +** Logging and Pretty Printing: ** + +* Printing functions have been removed from `Pp.mli`, which is now a + purely pretty-printing interface. Functions affected are: + +```` ocaml +val pp : std_ppcmds -> unit +val ppnl : std_ppcmds -> unit +val pperr : std_ppcmds -> unit +val pperrnl : std_ppcmds -> unit +val pperr_flush : unit -> unit +val pp_flush : unit -> unit +val flush_all : unit -> unit +val msg : std_ppcmds -> unit +val msgnl : std_ppcmds -> unit +val msgerr : std_ppcmds -> unit +val msgerrnl : std_ppcmds -> unit +val message : string -> unit +```` + + which are no more available. Users of `Pp.pp msg` should now use the + proper `Feedback.msg_*` function. Clients also have no control over + flushing, the back end takes care of it. + +* Feedback related functions and definitions have been moved to the + `Feedback` module. `message_level` has been renamed to + level. Functions moved from Pp to Feedback are: + +```` ocaml +val set_logger : logger -> unit +val std_logger : logger +val emacs_logger : logger +val feedback_logger : logger +```` + +* We now provide several loggers, `log_via_feedback` is removed in + favor of `set_logger feedback_logger`. Output functions are: + +```` ocaml +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b +val msg_info : Pp.std_ppcmds -> unit +val msg_notice : Pp.std_ppcmds -> unit +val msg_warning : Pp.std_ppcmds -> unit +val msg_error : Pp.std_ppcmds -> unit +val msg_debug : Pp.std_ppcmds -> unit +```` + + with the `msg_*` functions being just an alias for `logger $Level`. + +* The main feedback functions are: + +```` ocaml +val set_feeder : (feedback -> unit) -> unit +val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit +val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit +```` + Note that `feedback` doesn't take two parameters anymore. After + refactoring the following function has been removed: + +```` ocaml +val get_id_for_feedback : unit -> edit_or_state_id * route_id +```` + - The interface of the Context module was changed. Related types and functions were put in separate submodules. The mapping from old identifiers to new identifiers is the following: diff --git a/dev/printers.mllib b/dev/printers.mllib index aa74cb508..0957197cc 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -26,16 +26,17 @@ Control Loc Serialize Stateid -Feedback -Pp -Segmenttree -Unicodetable -Unicode CObj CArray CStack Util +Pp Ppstyle +Richpp +Feedback +Segmenttree +Unicodetable +Unicode Errors Bigint CUnix diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f5599d793..4da901e53 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,7 +29,8 @@ let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) -let pppp x = pp x +let pp x = Feedback.msg_notice x +let pppp x = Feedback.msg_notice x (** Future printer *) @@ -315,7 +316,7 @@ let constr_display csr = | Anonymous -> "Anonymous" in - Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush () + Feedback.msg_notice (str (term_display csr) ++fnl ()) open Format;; @@ -515,7 +516,7 @@ let _ = (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Pp.pp (Errors.print e) + e -> Feedback.msg_notice (Errors.print e) let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; @@ -531,7 +532,7 @@ let _ = (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Pp.pp (Errors.print e) + e -> Feedback.msg_notice (Errors.print e) let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 1c501df80..afa94a63e 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -79,7 +79,7 @@ and ppwhd whd = | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s - | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl) + | Vuniv_level lvl -> Feedback.msg_notice (Univ.Level.pr lvl) and ppvblock b = open_hbox(); diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index d67f1eee3..64be07b9c 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -104,11 +104,11 @@ struct 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 print_debug s = make (fun _ -> Feedback.msg_info s) + let print_info s = make (fun _ -> Feedback.msg_info s) + let print_warning s = make (fun _ -> Feedback.msg_warning s) + let print_error s = make (fun _ -> Feedback.msg_error s) + let print_notice s = make (fun _ -> Feedback.msg_notice s) let run = fun x -> try x () with Exception e as src -> diff --git a/engine/proofview.ml b/engine/proofview.ml index 45af16759..bcdd4da11 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -46,7 +46,7 @@ let compact el ({ solution } as pv) = evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in - msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); + Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); new_el, { pv with solution = new_solution; } @@ -857,7 +857,7 @@ let tclTIME s t = else str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking") in - msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++ + Feedback.msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++ System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in let rec aux n t = let open Proof in diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 4c4ecaf73..0791306c4 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -117,7 +117,7 @@ let declare_tactic loc s c cl = match cl with Tacenv.register_ml_tactic $se$ [|$tac$|]; Mltop.declare_cache_obj obj $plugin_name$; } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in tactic extend " ^ $entry$ ^": ")) (Errors.print e)) ]; } >> @@ -135,7 +135,7 @@ let declare_tactic loc s c cl = match cl with Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); Mltop.declare_cache_obj $obj$ $plugin_name$; } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in tactic extend " ^ $entry$ ^": ")) (Errors.print e)) ]; } >> diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 904662ea1..4060af8e4 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -128,7 +128,7 @@ let declare_command loc s c nt cl = CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) (Errors.print e)) ]; diff --git a/ide/coq.ml b/ide/coq.ml index fa0adf979..7a32faffc 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -291,17 +291,17 @@ let rec check_errors = function | `OUT :: _ -> raise (TubeError "OUT") let handle_intermediate_message handle xml = - let message = Pp.to_message xml in - let level = message.Pp.message_level in - let content = message.Pp.message_content in + let message = Feedback.to_message xml in + let level = message.Feedback.message_level in + let content = message.Feedback.message_content in let logger = match handle.waiting_for with | Some (_, l) -> l | None -> function - | Pp.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s) - | Pp.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) - | Pp.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s) - | Pp.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s) - | Pp.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s) + | Feedback.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s) + | Feedback.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) + | Feedback.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s) + | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s) + | Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s) in logger level (Richpp.richpp_of_xml content) @@ -335,7 +335,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = let l_end = Lexing.lexeme_end lex in state.fragment <- String.sub s l_end (String.length s - l_end); state.lexerror <- None; - if Pp.is_message xml then begin + if Feedback.is_message xml then begin handle_intermediate_message handle xml; loop () end else if Feedback.is_feedback xml then begin diff --git a/ide/coqOps.ml b/ide/coqOps.ml index b55786ddd..930135995 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -519,7 +519,7 @@ object(self) self#position_error_tag_at_iter start phrase loc; buffer#place_cursor ~where:stop; messages#clear; - messages#push Pp.Error msg; + messages#push Feedback.Error msg; self#show_goals end else self#show_goals_aux ~move_insert:true () @@ -595,7 +595,8 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - logger Pp.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted"); + + logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted"); self#discard_command_queue queue; conclude [] | `Skip(start,stop), (_,s) :: topstack -> @@ -611,7 +612,7 @@ object(self) let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; - logger Pp.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Richpp.richpp_of_string msg); self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> @@ -619,7 +620,7 @@ object(self) let topstack, _ = Doc.context document in self#exit_focus; self#cleanup (Doc.cut_at document tip); - logger Pp.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Richpp.richpp_of_string msg); self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) @@ -638,7 +639,7 @@ object(self) let next = function | Good _ -> messages#clear; - messages#push Pp.Info (Richpp.richpp_of_string "All proof terms checked by the kernel"); + messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel"); Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status ~logger:messages#push true) next @@ -740,8 +741,8 @@ object(self) self#cleanup (Doc.cut_at document to_id); conclusion () | Fail (safe_id, loc, msg) -> - if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC"); - messages#push Pp.Error msg; + if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); + messages#push Feedback.Error msg; if Stateid.equal safe_id Stateid.dummy then self#show_goals else undo safe_id (Doc.focused document && Doc.is_in_focus document safe_id)) @@ -759,7 +760,7 @@ object(self) ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = messages#clear; - messages#push Pp.Error msg; + messages#push Feedback.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) else diff --git a/ide/coqide.ml b/ide/coqide.ml index 1fe393d2b..758a5a4c9 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -783,7 +783,7 @@ let coqtop_arguments sn = let args = String.concat " " args in let msg = Printf.sprintf "Invalid arguments: %s" args in let () = sn.messages#clear in - sn.messages#push Pp.Error (Richpp.richpp_of_string msg) + sn.messages#push Feedback.Error (Richpp.richpp_of_string msg) else dialog#destroy () in let _ = entry#connect#activate ok_cb in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9a3e85e47..59efc2d82 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -98,11 +98,11 @@ let coqide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then - msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then - msg_warning (strbrk "Rather use CoqIDE navigation instead"); + Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then - msg_warning (strbrk "Query commands should not be inserted in scripts") + Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts") (** Interpretation (cf. [Ide_intf.interp]) *) @@ -212,7 +212,7 @@ let export_pre_goals pgs = let goals () = Stm.finish (); let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); + if not (String.is_empty s) then Feedback.msg_info (str s); try let pfts = Proof_global.give_me_the_proof () in Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) @@ -222,7 +222,7 @@ let evars () = try Stm.finish (); let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); + if not (String.is_empty s) then Feedback.msg_info (str s); let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in @@ -255,7 +255,7 @@ let status force = Stm.finish (); if force then Stm.join (); let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); + if not (String.is_empty s) then Feedback.msg_info (str s); let path = let l = Names.DirPath.repr (Lib.cwd ()) in List.rev_map Names.Id.to_string l @@ -445,11 +445,11 @@ let slave_logger xml_oc level message = (* convert the message into XML *) let msg = hov 0 message in let message = { - Pp.message_level = level; - Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg)); + Feedback.message_level = level; + Feedback.message_content = (Richpp.repr (Richpp.richpp_of_pp msg)); } in let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in - let xml = Pp.of_message message in + let xml = Feedback.of_message message in print_xml xml_oc xml let slave_feeder xml_oc msg = @@ -471,8 +471,8 @@ let loop () = CThread.thread_friendly_read in_ch s ~off:0 ~len) in let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in - set_logger (slave_logger xml_oc); - set_feeder (slave_feeder xml_oc); + Feedback.set_logger (slave_logger xml_oc); + Feedback.set_feeder (slave_feeder xml_oc); (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; @@ -482,7 +482,7 @@ let loop () = (* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in let () = pr_debug_call q in - let r = eval_call xml_oc (slave_logger xml_oc Pp.Notice) q in + let r = eval_call xml_oc (slave_logger xml_oc Feedback.Notice) q in let () = pr_debug_answer q r in (* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *) print_xml xml_oc (Xmlprotocol.of_answer q r); diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 508881cad..00c3f88e5 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -297,15 +297,15 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Pp.message_level -> Richpp.richpp -> unit +type logger = Feedback.level -> Richpp.richpp -> unit let default_logger level message = let level = match level with - | Pp.Debug _ -> `DEBUG - | Pp.Info -> `INFO - | Pp.Notice -> `NOTICE - | Pp.Warning -> `WARNING - | Pp.Error -> `ERROR + | Feedback.Debug _ -> `DEBUG + | Feedback.Info -> `INFO + | Feedback.Notice -> `NOTICE + | Feedback.Warning -> `WARNING + | Feedback.Error -> `ERROR in Minilib.log ~level (xml_to_string message) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 4e35a6f9f..491e8e823 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -69,7 +69,7 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Pp.message_level -> Richpp.richpp -> unit +type logger = Feedback.level -> Richpp.richpp -> unit val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 081094e2b..de0720e03 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -56,24 +56,24 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) | ("-full"|"-opt") :: r -> process_cmd_line orig_dir (project_file,makefile,install,true) l r | "-impredicative-set" :: r -> - Pp.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."); + Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."); process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r | "-no-install" :: r -> - Pp.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead"))); + Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead"))); process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r | "-install" :: d :: r -> - if install <> UnspecInstall then Pp.msg_warning (Pp.str "-install sets more than once."); + if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once."); let install = match d with | "user" -> UserInstall | "none" -> NoInstall | "global" -> TraditionalInstall - | _ -> Pp.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install."))); + | _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install."))); install in process_cmd_line orig_dir (project_file,makefile,install,opt) l r | "-custom" :: com :: dependencies :: file :: r -> - Pp.msg_warning (Pp.app + Feedback.msg_warning (Pp.app (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".") (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.") ); @@ -94,7 +94,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match project_file with | None -> () - | Some _ -> Pp.msg_warning (Pp.str + | Some _ -> Feedback.msg_warning (Pp.str "Several features will not work with multiple project files.") in let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in @@ -109,7 +109,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) let () = match makefile with |None -> () |Some f -> - Pp.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be."))) + Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be."))) in process_cmd_line orig_dir (project_file,Some file,install,opt) l r end | v :: "=" :: def :: r -> diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 7728ad236..758f383d6 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -73,8 +73,8 @@ let message_view () : message_view = method push level msg = let tags = match level with - | Pp.Error -> [Tags.Message.error] - | Pp.Warning -> [Tags.Message.warning] + | Feedback.Error -> [Tags.Message.error] + | Feedback.Warning -> [Tags.Message.warning] | _ -> [] in let rec non_empty = function @@ -88,7 +88,7 @@ let message_view () : message_view = push#call (level, msg) end - method add msg = self#push Pp.Notice msg + method add msg = self#push Feedback.Notice msg method add_string s = self#add (Richpp.richpp_of_string s) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0de98242a..4a451634d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1069,7 +1069,7 @@ let alias_of als = match als.alias_ids with | id :: _ -> Name id let message_redundant_alias id1 id2 = - msg_warning + Feedback.msg_warning (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) (** {6 Expanding notations } diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 85212b7ab..931fc1ca4 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -141,7 +141,7 @@ let interval loc = let dump_ref loc filepath modpath ident ty = match !glob_output with | Feedback -> - Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) + Feedback.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) | NoGlob -> () | _ when not (Loc.is_ghost loc) -> let bl,el = interval loc in @@ -240,7 +240,7 @@ let dump_binding loc id = () let dump_def ty loc secpath id = if !glob_output = Feedback then - Pp.feedback (Feedback.GlobDef (loc, id, secpath, ty)) + Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty)) else let bl,el = interval loc in dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 751b03a4a..567150a5d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -310,7 +310,7 @@ let implicits_of_glob_constr ?(with_products=true) l = else let () = match bk with | Implicit -> - msg_warning (strbrk "Ignoring implicit status of product binder " ++ + Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ pr_name na ++ strbrk " and following binders") | _ -> () in [] diff --git a/interp/notation.ml b/interp/notation.ml index 0a65dfc09..b19fd9e1f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -184,7 +184,7 @@ let declare_delimiters scope key = | None -> scope_map := String.Map.add scope newsc !scope_map | Some oldkey when String.equal oldkey key -> () | Some oldkey -> - msg_warning + Feedback.msg_warning (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map end; @@ -192,7 +192,7 @@ let declare_delimiters scope key = let oldscope = String.Map.find key !delimiters_map in if String.equal oldscope scope then () else begin - msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); + Feedback.msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); delimiters_map := String.Map.add key scope !delimiters_map end with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map @@ -201,7 +201,7 @@ let remove_delimiters scope = let sc = find_scope scope in let newsc = { sc with delimiters = None } in match sc.delimiters with - | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".") + | None -> Feedback.msg_warning (str "No bound key for scope " ++ str scope ++ str ".") | Some key -> scope_map := String.Map.add scope newsc !scope_map; try @@ -388,7 +388,7 @@ let declare_notation_interpretation ntn scopt pat df = let which_scope = match scopt with | None -> mt () | Some _ -> str " in scope " ++ str scope in - msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope) + Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope) in let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in let () = scope_map := String.Map.add scope sc !scope_map in diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index db548ec32..891b64fa1 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -93,7 +93,7 @@ let is_verbose_compat () = let verbose_compat kn def = function | Some v when is_verbose_compat () && Flags.version_strictly_greater v -> let act = - if !verbose_compat_notations then msg_warning else errorlabstrm "" + if !verbose_compat_notations then Feedback.msg_warning else errorlabstrm "" in let pp_def = match def with | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 42538925a..91099bbb1 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -132,7 +132,7 @@ let fold_constr_expr_with_binders g f n acc = function fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (loc,_,_) -> - msg_warning (strbrk "Capture check in multiple binders not done"); acc + Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc let free_vars_of_constr_expr c = let rec aux bdvars l = function diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 77eac9ee9..431c914c0 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -904,10 +904,10 @@ let compile fail_on_error ?universes:(universes=0) env c = in let fv = List.rev (!(reloc.in_env).fv_rev) in (if !Flags.dump_bytecode then - Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ; + Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> - let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in + let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ Id.print tname ++ str str_max_constructors)); diff --git a/kernel/closure.ml b/kernel/closure.ml index bf3801e54..65123108f 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -45,7 +45,7 @@ let reset () = prune := 0 let stop() = - msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ + Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]") diff --git a/kernel/names.ml b/kernel/names.ml index e8226d3d3..9abc9842a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -36,7 +36,7 @@ struct let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then Errors.error x else if warn then Pp.msg_warning (str x) + if fatal then Errors.error x else if warn then Feedback.msg_warning (str x) in Option.iter iter (Unicode.ident_refutation x) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 79e5d3af0..44cf21cff 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1863,7 +1863,7 @@ let compile_constant env sigma prefix ~interactive con cb = | Def t -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in - if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code"); + if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); let is_lazy = is_lazy prefix t in let code = if is_lazy then mk_lazy code else code in let name = @@ -1878,11 +1878,11 @@ let compile_constant env sigma prefix ~interactive con cb = let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in (auxdefs,mkMLlam [|univ|] code) in - if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code"); + if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code"); let code = optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs) in - if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code"); + if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code"); code, name | _ -> let i = push_symbol (SymbConst con) in diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 4ed926f1f..a0ff9e123 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -134,12 +134,12 @@ let native_conv_gen pb sigma env univs t1 t2 = match compile ml_filename code with | (true, fn) -> begin - if !Flags.debug then Pp.msg_debug (Pp.str "Running test..."); + if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); let t0 = Sys.time () in call_linker ~fatal:true prefix fn (Some upds); let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Pp.msg_debug (Pp.str time_info); + if !Flags.debug then Feedback.msg_debug (Pp.str time_info); (* TODO change 0 when we can have deBruijn *) fst (conv_val env pb 0 !rt1 !rt2 univs) end @@ -149,7 +149,7 @@ let native_conv_gen pb sigma env univs t1 t2 = let native_conv cv_pb sigma env t1 t2 = if Coq_config.no_native_compiler then begin let msg = "Native compiler is disabled, falling back to VM conversion test." in - Pp.msg_warning (Pp.str msg); + Feedback.msg_warning (Pp.str msg); vm_conv cv_pb env t1 t2 end else diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 4296b73ab..5b92e9554 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -73,20 +73,20 @@ let call_compiler ml_filename = ::"-w"::"a" ::include_dirs @ ["-impl"; ml_filename] in - if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); + if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (ocamlfind ()) args in let res = match res with | Unix.WEXITED 0 -> true | Unix.WEXITED n -> - Pp.(msg_warning (str "command exited with status " ++ int n)); false + Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false | Unix.WSIGNALED n -> - Pp.(msg_warning (str "command killed by signal " ++ int n)); false + Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false | Unix.WSTOPPED n -> - Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in + Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in res, link_filename with Unix.Unix_error (e,_,_) -> - Pp.(msg_warning (str (Unix.error_message e))); + Feedback.msg_warning Pp.(str (Unix.error_message e)); false, link_filename let compile fn code = @@ -120,7 +120,7 @@ let call_linker ?(fatal=true) prefix f upds = begin let msg = "Cannot find native compiler file " ^ f in if fatal then Errors.error msg - else if !Flags.debug then Pp.msg_debug (Pp.str msg) + else if !Flags.debug then Feedback.msg_debug (Pp.str msg) end else (try @@ -129,8 +129,8 @@ let call_linker ?(fatal=true) prefix f upds = with Dynlink.Error e as exn -> let exn = Errors.push exn in let msg = "Dynlink error, " ^ Dynlink.error_message e in - if fatal then (Pp.msg_error (Pp.str msg); iraise exn) - else if !Flags.debug then Pp.msg_debug (Pp.str msg)); + if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) + else if !Flags.debug then Feedback.msg_debug (Pp.str msg)); match upds with Some upds -> update_locations upds | _ -> () let link_library ~prefix ~dirname ~basename = diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 9d159be64..246b00da4 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -29,13 +29,13 @@ and translate_field prefix mp env acc (l,x) = let con = make_con mp empty_dirpath l in (if !Flags.debug then let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in - Pp.msg_debug (Pp.str msg)); + Feedback.msg_debug (Pp.str msg)); compile_constant_field (pre_env env) prefix con acc cb | SFBmind mb -> (if !Flags.debug then let id = mb.mind_packets.(0).mind_typename in let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in - Pp.msg_debug (Pp.str msg)); + Feedback.msg_debug (Pp.str msg)); compile_mind_field prefix mp l acc mb | SFBmodule md -> let mp = md.mod_mp in @@ -43,7 +43,7 @@ and translate_field prefix mp env acc (l,x) = let msg = Printf.sprintf "Compiling module %s..." (ModPath.to_string mp) in - Pp.msg_debug (Pp.str msg)); + Feedback.msg_debug (Pp.str msg)); translate_mod prefix mp env md.mod_type acc | SFBmodtype mdtyp -> let mp = mdtyp.mod_mp in @@ -51,11 +51,11 @@ and translate_field prefix mp env acc (l,x) = let msg = Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp) in - Pp.msg_debug (Pp.str msg)); + Feedback.msg_debug (Pp.str msg)); translate_mod prefix mp env mdtyp.mod_type acc let dump_library mp dp env mod_expr = - if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library..."); + if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library..."); match mod_expr with | NoFunctor struc -> let env = add_structure mp struc empty_delta_resolver env in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5bf369441..30a346c91 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -681,7 +681,7 @@ let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); + Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); gen_conv cv_pb env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3839135a8..6bfd2457a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -167,8 +167,10 @@ let hcons_j j = { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} let feedback_completion_typecheck = - Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) - + let open Feedback in + Option.iter (fun state_id -> + feedback ~id:(State state_id) Feedback.Complete) + let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 89e833254..53db6f5be 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -185,7 +185,7 @@ let vm_conv_gen cv_pb env univs t1 t2 = let v2 = val_of_constr env t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) with Not_found | Invalid_argument _ -> - (Pp.msg_warning + (Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to default conversion"); Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) full_transparent_state env univs t1 t2) diff --git a/lib/aux_file.ml b/lib/aux_file.ml index f7bd81f85..d06d4b376 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -88,7 +88,7 @@ let load_aux_file_for vfile = | Sys_error s | Scanf.Scan_failure s | Failure s | Invalid_argument s -> Flags.if_verbose - Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s); + Feedback.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s); empty_aux_file let set h loc k v = set h (Loc.unloc loc) k v diff --git a/lib/clib.mllib b/lib/clib.mllib index 3c1c5da33..c3ec4a696 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -28,13 +28,14 @@ CArray CStack Util Stateid -Feedback Pp Ppstyle +Xml_datatype +Richpp +Feedback Xml_lexer Xml_parser Xml_printer -Richpp CUnix Envars Aux_file diff --git a/lib/explore.ml b/lib/explore.ml index 587db1156..aa7bddf2b 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -27,7 +27,7 @@ module Make = functor(S : SearchProblem) -> struct | [i] -> int i | i :: l -> pp_rec l ++ str "." ++ int i in - msg_debug (h 0 (pp_rec p) ++ pp) + Feedback.msg_debug (h 0 (pp_rec p) ++ pp) (*s Depth first search. *) diff --git a/lib/feedback.ml b/lib/feedback.ml index 1a90685de..dce4372ec 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -9,7 +9,7 @@ open Xml_datatype open Serialize -type message_level = +type level = | Debug of string | Info | Notice @@ -17,7 +17,7 @@ type message_level = | Error type message = { - message_level : message_level; + message_level : level; message_content : xml; } @@ -169,3 +169,129 @@ let is_feedback = function | _ -> false let default_route = 0 + +(** Feedback and logging *) +open Pp +open Pp_control + +type logger = level -> std_ppcmds -> unit + +let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) +let msgnl strm = msgnl_with !std_ft strm + +(* XXX: This is really painful! *) +module Emacs = struct + + (* Special chars for emacs, to detect warnings inside goal output *) + let emacs_quote_start = String.make 1 (Char.chr 254) + let emacs_quote_end = String.make 1 (Char.chr 255) + + let emacs_quote_err g = + hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) + + let emacs_quote_info_start = "" + let emacs_quote_info_end = "" + + let emacs_quote_info g = + hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) + +end + +open Emacs + +let dbg_str = str "Debug:" ++ spc () +let info_str = mt () +let warn_str = str "Warning:" ++ spc () +let err_str = str "Error:" ++ spc () + +let make_body quoter info s = quoter (hov 0 (info ++ s)) + +(* Generic logger *) +let gen_logger dbg err level msg = match level with + | Debug _ -> msgnl (make_body dbg dbg_str msg) + | Info -> msgnl (make_body dbg info_str msg) + | Notice -> msgnl msg + | Warning -> Flags.if_warn (fun () -> + msgnl_with !err_ft (make_body err warn_str msg)) () + | Error -> msgnl_with !err_ft (make_body err err_str msg) + +(** Standard loggers *) +let std_logger = gen_logger (fun x -> x) (fun x -> x) + +(* Color logger *) +let color_terminal_logger level strm = + let msg = Ppstyle.color_msg in + match level with + | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm + | Info -> msg !std_ft strm + | Notice -> msg !std_ft strm + | Warning -> + let header = ("Warning", Ppstyle.warning_tag) in + Flags.if_warn (fun () -> msg ~header !err_ft strm) () + | Error -> msg ~header:("Error", Ppstyle.error_tag) !err_ft strm + +(* Rules for emacs: + - Debug/info: emacs_quote_info + - Warning/Error: emacs_quote_err + - Notice: unquoted + *) +let emacs_logger = gen_logger emacs_quote_info emacs_quote_err + +let logger = ref std_logger +let set_logger l = logger := l + +let msg_info x = !logger Info x +let msg_notice x = !logger Notice x +let msg_warning x = !logger Warning x +let msg_error x = !logger Error x +let msg_debug x = !logger (Debug "_") x + +(** Feeders *) +let feeder = ref ignore +let set_feeder f = feeder := f + +let feedback_id = ref (Edit 0) +let feedback_route = ref default_route + +let set_id_for_feedback ?(route=default_route) i = + feedback_id := i; feedback_route := route + +let feedback ?id ?route what = + !feeder { + contents = what; + route = Option.default !feedback_route route; + id = Option.default !feedback_id id; + } + +let feedback_logger lvl msg = + feedback ~route:!feedback_route ~id:!feedback_id ( + Message { + message_level = lvl; + message_content = Richpp.of_richpp (Richpp.richpp_of_pp msg); + }) + +(* Output to file *) +let ft_logger old_logger ft level mesg = + let id x = x in + match level with + | Debug _ -> msgnl_with ft (make_body id dbg_str mesg) + | Info -> msgnl_with ft (make_body id info_str mesg) + | Notice -> msgnl_with ft mesg + | Warning -> old_logger level mesg + | Error -> old_logger level mesg + +let with_output_to_file fname func input = + let old_logger = !logger in + let channel = open_out (String.concat "." [fname; "out"]) in + logger := ft_logger old_logger (Format.formatter_of_out_channel channel); + try + let output = func input in + logger := old_logger; + close_out channel; + output + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + logger := old_logger; + close_out channel; + Exninfo.iraise reraise + diff --git a/lib/feedback.mli b/lib/feedback.mli index 0d8e20230..1e96f9a49 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -9,7 +9,7 @@ open Xml_datatype (* Old plain messages (used to be in Pp) *) -type message_level = +type level = | Debug of string | Info | Notice @@ -17,7 +17,7 @@ type message_level = | Error type message = { - message_level : message_level; + message_level : level; message_content : xml; } @@ -66,3 +66,80 @@ val of_feedback : feedback -> xml val to_feedback : xml -> feedback val is_feedback : xml -> bool +(** {6 Feedback sent, even asynchronously, to the user interface} *) + +(** Moved here from pp.ml *) + +(* Morally the parser gets a string and an edit_id, and gives back an AST. + * Feedbacks during the parsing phase are attached to this edit_id. + * The interpreter assignes an exec_id to the ast, and feedbacks happening + * during interpretation are attached to the exec_id. + * Only one among state_id and edit_id can be provided. *) + +(** A [logger] takes a level plus a pretty printing doc and logs it *) +type logger = level -> Pp.std_ppcmds -> unit + +(** [set_logger l] makes the [msg_*] to use [l] for logging *) +val set_logger : logger -> unit + +(** [std_logger] standard logger to [stdout/stderr] *) +val std_logger : logger + +val color_terminal_logger : logger +(* This logger will apply the proper {!Pp_style} tags, and in + particular use the formatters {!Pp_control.std_ft} and + {!Pp_control.err_ft} to display those messages. Be careful this is + not compatible with the Emacs mode! *) + +(** [feedback_logger] will produce feedback messages instead IO events *) +val feedback_logger : logger +val emacs_logger : logger + + +(** [set_feeder] A feeder processes the feedback, [ignore] by default *) +val set_feeder : (feedback -> unit) -> unit + +(** [feedback ?id ?route fb] produces feedback fb, with [route] and + [id] set appropiatedly, if absent, it will use the defaults set by + [set_id_for_feedback] *) +val feedback : + ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit + +(** [set_id_for_feedback route id] Set the defaults for feedback *) +val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit + +(** [with_output_to_file file f x] executes [f x] with logging + redirected to a file [file] *) +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b + +(** {6 output functions} + +[msg_notice] do not put any decoration on output by default. If +possible don't mix it with goal output (prefer msg_info or +msg_warning) so that interfaces can dispatch outputs easily. Once all +interfaces use the xml-like protocol this constraint can be +relaxed. *) +(* Should we advertise these functions more? Should they be the ONLY + allowed way to output something? *) + +val msg_info : Pp.std_ppcmds -> unit +(** Message that displays information, usually in verbose mode, such as [Foobar + is defined] *) + +val msg_notice : Pp.std_ppcmds -> unit +(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) + +val msg_warning : Pp.std_ppcmds -> unit +(** Message indicating that something went wrong, but without serious + consequences. *) + +val msg_error : Pp.std_ppcmds -> unit +(** Message indicating that something went really wrong, though still + recoverable; otherwise an exception would have been raised. *) + +val msg_debug : Pp.std_ppcmds -> unit +(** For debugging purposes *) + + + + diff --git a/lib/pp.ml b/lib/pp.ml index e4c78ba73..d07f01b90 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -64,13 +64,6 @@ end open Pp_control -(* This should not be used outside of this file. Use - Flags.print_emacs instead. This one is updated when reading - command line options. This was the only way to make [Pp] depend on - an option without creating a circularity: [Flags] -> [Util] -> - [Pp] -> [Flags] *) -let print_emacs = ref false - (* The different kinds of blocks are: \begin{description} \item[hbox:] Horizontal block no line breaking; @@ -339,175 +332,23 @@ let pp_dirs ?pp_tag ft = let () = Format.pp_print_flush ft () in Exninfo.iraise reraise - - -(* pretty print on stdout and stderr *) - -(* Special chars for emacs, to detect warnings inside goal output *) -let emacs_quote_start = String.make 1 (Char.chr 254) -let emacs_quote_end = String.make 1 (Char.chr 255) - -let emacs_quote_info_start = "" -let emacs_quote_info_end = "" - -let emacs_quote g = - if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) - else hov 0 g - -let emacs_quote_info g = - if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) - else hov 0 g - - (* pretty printing functions WITHOUT FLUSH *) let pp_with ?pp_tag ft strm = pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm)) -let ppnl_with ft strm = - pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ()))) - (* pretty printing functions WITH FLUSH *) let msg_with ft strm = pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) -let msgnl_with ft strm = - pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_newline)) - -(* pretty printing functions WITHOUT FLUSH *) -let pp x = pp_with !std_ft x -let ppnl x = ppnl_with !std_ft x -let pperr x = pp_with !err_ft x -let pperrnl x = ppnl_with !err_ft x -let message s = ppnl (str s) -let pp_flush x = Format.pp_print_flush !std_ft x -let pperr_flush x = Format.pp_print_flush !err_ft x -let flush_all () = - flush stderr; flush stdout; pp_flush (); pperr_flush () - -(* pretty printing functions WITH FLUSH *) -let msg x = msg_with !std_ft x -let msgnl x = msgnl_with !std_ft x -let msgerr x = msg_with !err_ft x -let msgerrnl x = msgnl_with !err_ft x - -(* Logging management *) - -type message_level = Feedback.message_level = - | Debug of string - | Info - | Notice - | Warning - | Error - -type message = Feedback.message = { - message_level : message_level; - message_content : Xml_datatype.xml; -} - -let of_message = Feedback.of_message -let to_message = Feedback.to_message -let is_message = Feedback.is_message - -type logger = message_level -> std_ppcmds -> unit - -let make_body info s = - emacs_quote (hov 0 (info ++ spc () ++ s)) - -let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm)) -let warnbody strm = make_body (str "Warning:") strm -let errorbody strm = make_body (str "Error:") strm -let infobody strm = emacs_quote_info strm - -let std_logger ~id:_ level msg = match level with -| Debug _ -> msgnl (debugbody msg) -| Info -> msgnl (hov 0 msg) -| Notice -> msgnl msg -| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) () -| Error -> msgnl_with !err_ft (errorbody msg) - -let emacs_logger ~id:_ level mesg = match level with -| Debug _ -> msgnl (debugbody mesg) -| Info -> msgnl (infobody mesg) -| Notice -> msgnl mesg -| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody mesg)) () -| Error -> msgnl_with !err_ft (errorbody mesg) - -let logger = ref std_logger - -let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger -let make_pp_nonemacs() = print_emacs:=false; logger := std_logger - -let ft_logger old_logger ft ~id level mesg = match level with - | Debug _ -> msgnl_with ft (debugbody mesg) - | Info -> msgnl_with ft (infobody mesg) - | Notice -> msgnl_with ft mesg - | Warning -> old_logger ~id:id level mesg - | Error -> old_logger ~id:id level mesg - -let with_output_to_file fname func input = - let old_logger = !logger in - let channel = open_out (String.concat "." [fname; "out"]) in - logger := ft_logger old_logger (Format.formatter_of_out_channel channel); - try - let output = func input in - logger := old_logger; - close_out channel; - output - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - logger := old_logger; - close_out channel; - Exninfo.iraise reraise - -let feedback_id = ref (Feedback.Edit 0) -let feedback_route = ref Feedback.default_route - (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch them to different windows. *) -let msg_info x = !logger ~id:!feedback_id Info x -let msg_notice x = !logger ~id:!feedback_id Notice x -let msg_warning x = !logger ~id:!feedback_id Warning x -let msg_error x = !logger ~id:!feedback_id Error x -let msg_debug x = !logger ~id:!feedback_id (Debug "_") x - -let set_logger l = logger := (fun ~id:_ lvl msg -> l lvl msg) - -let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg - -(** Feedback *) - -let feeder = ref ignore -let set_id_for_feedback ?(route=Feedback.default_route) i = - feedback_id := i; feedback_route := route -let feedback ?state_id ?edit_id ?route what = - !feeder { - Feedback.contents = what; - Feedback.route = Option.default !feedback_route route; - Feedback.id = - match state_id, edit_id with - | Some id, _ -> Feedback.State id - | None, Some eid -> Feedback.Edit eid - | None, None -> !feedback_id; - } -let set_feeder f = feeder := f -let get_id_for_feedback () = !feedback_id, !feedback_route - -(** Utility *) - +(** Output to a string formatter *) let string_of_ppcmds c = - msg_with Format.str_formatter c; + Format.fprintf Format.str_formatter "@[%a@]" msg_with c; Format.flush_str_formatter () -let log_via_feedback printer = logger := (fun ~id lvl msg -> - !feeder { - Feedback.contents = Feedback.Message { - message_level = lvl; - message_content = printer msg }; - Feedback.route = !feedback_route; - Feedback.id = id }) - (* Copy paste from Util *) let pr_comma () = str "," ++ spc () @@ -597,3 +438,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v let prvect elem v = prvect_with_sep mt elem v let surround p = hov 1 (str"(" ++ p ++ str")") + diff --git a/lib/pp.mli b/lib/pp.mli index 04a60a7c8..ced4b6603 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -6,32 +6,24 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Modify pretty printing functions behavior for emacs ouput (special - chars inserted at some places). This function should called once in - module [Options], that's all. *) -val make_pp_emacs:unit -> unit -val make_pp_nonemacs:unit -> unit - -val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b - (** Pretty-printers. *) type std_ppcmds (** {6 Formatting commands} *) -val str : string -> std_ppcmds +val str : string -> std_ppcmds val stras : int * string -> std_ppcmds -val brk : int * int -> std_ppcmds -val tbrk : int * int -> std_ppcmds -val tab : unit -> std_ppcmds -val fnl : unit -> std_ppcmds -val pifb : unit -> std_ppcmds -val ws : int -> std_ppcmds -val mt : unit -> std_ppcmds -val ismt : std_ppcmds -> bool - -val comment : int -> std_ppcmds +val brk : int * int -> std_ppcmds +val tbrk : int * int -> std_ppcmds +val tab : unit -> std_ppcmds +val fnl : unit -> std_ppcmds +val pifb : unit -> std_ppcmds +val ws : int -> std_ppcmds +val mt : unit -> std_ppcmds +val ismt : std_ppcmds -> bool + +val comment : int -> std_ppcmds val comments : ((int * int) * string) list ref (** {6 Manipulation commands} *) @@ -100,87 +92,10 @@ sig (** Project an object from a tag. *) end -type tag_handler = Tag.t -> Format.tag - val tag : Tag.t -> std_ppcmds -> std_ppcmds val open_tag : Tag.t -> std_ppcmds val close_tag : unit -> std_ppcmds -(** {6 Sending messages to the user} *) -type message_level = Feedback.message_level = - | Debug of string - | Info - | Notice - | Warning - | Error - -type message = Feedback.message = { - message_level : message_level; - message_content : Xml_datatype.xml; -} - -type logger = message_level -> std_ppcmds -> unit - -(** {6 output functions} - -[msg_notice] do not put any decoration on output by default. If -possible don't mix it with goal output (prefer msg_info or -msg_warning) so that interfaces can dispatch outputs easily. Once all -interfaces use the xml-like protocol this constraint can be -relaxed. *) -(* Should we advertise these functions more? Should they be the ONLY - allowed way to output something? *) - -val msg_info : std_ppcmds -> unit -(** Message that displays information, usually in verbose mode, such as [Foobar - is defined] *) - -val msg_notice : std_ppcmds -> unit -(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) - -val msg_warning : std_ppcmds -> unit -(** Message indicating that something went wrong, but without serious - consequences. *) - -val msg_error : std_ppcmds -> unit -(** Message indicating that something went really wrong, though still - recoverable; otherwise an exception would have been raised. *) - -val msg_debug : std_ppcmds -> unit -(** For debugging purposes *) - -val std_logger : logger -(** Standard logging function *) - -val set_logger : logger -> unit - -val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit - -val of_message : message -> Xml_datatype.xml -val to_message : Xml_datatype.xml -> message -val is_message : Xml_datatype.xml -> bool - - -(** {6 Feedback sent, even asynchronously, to the user interface} *) - -(* This stuff should be available to most of the system, line msg_* above. - * But I'm unsure this is the right place, especially for the global edit_id. - * - * Morally the parser gets a string and an edit_id, and gives back an AST. - * Feedbacks during the parsing phase are attached to this edit_id. - * The interpreter assigns an exec_id to the ast, and feedbacks happening - * during interpretation are attached to the exec_id. - * Only one among state_id and edit_id can be provided. *) - -val feedback : - ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id -> - ?route:Feedback.route_id -> Feedback.feedback_content -> unit - -val set_id_for_feedback : - ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit -val set_feeder : (Feedback.feedback -> unit) -> unit -val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id - (** {6 Utilities} *) val string_of_ppcmds : std_ppcmds -> string @@ -251,31 +166,9 @@ val surround : std_ppcmds -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds -(** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *) - -val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit +(** {6 Low-level pretty-printing functions with and without flush} *) -(** {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 pperr_flush : unit -> unit -val pp_flush : unit -> unit -val flush_all: unit -> unit - -(** {6 Deprecated functions} *) - -(** DEPRECATED. Do not use in newly written code. *) - -val msg_with : Format.formatter -> std_ppcmds -> unit - -val msg : std_ppcmds -> unit -val msgnl : std_ppcmds -> unit -val msgerr : std_ppcmds -> unit -val msgerrnl : std_ppcmds -> unit -val message : string -> unit (** = pPNL *) +(** FIXME: These ignore the logging settings and call [Format] directly *) +type tag_handler = Tag.t -> Format.tag +val msg_with : Format.formatter -> std_ppcmds -> unit +val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index 3ecaac039..b068788c9 100644 --- a/lib/ppstyle.ml +++ b/lib/ppstyle.ml @@ -107,8 +107,11 @@ let pp_tag t = match Pp.Tag.prj t tag with | None -> "" | Some key -> key +let clear_tag_fn = ref (fun () -> ()) + let init_color_output () = let push_tag, pop_tag, clear_tag = make_style_stack !tags in + clear_tag_fn := clear_tag; let tag_handler = { Format.mark_open_tag = push_tag; Format.mark_close_tag = pop_tag; @@ -116,34 +119,23 @@ let init_color_output () = Format.print_close_tag = ignore; } in let open Pp_control in - let () = Format.pp_set_mark_tags !std_ft true in - let () = Format.pp_set_mark_tags !err_ft true in - let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in - let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in + Format.pp_set_mark_tags !std_ft true; + Format.pp_set_mark_tags !err_ft true; + Format.pp_set_formatter_tag_functions !std_ft tag_handler; + Format.pp_set_formatter_tag_functions !err_ft tag_handler + +let color_msg ?header ft strm = let pptag = tag in let open Pp in - let msg ?header ft strm = - let strm = match header with + let strm = match header with | None -> hov 0 strm | Some (h, t) -> let tag = Pp.Tag.inj t pptag in let h = Pp.tag tag (str h ++ str ":") in hov 0 (h ++ spc () ++ strm) - in - pp_with ~pp_tag ft strm; - Format.pp_print_newline ft (); - Format.pp_print_flush ft (); - (** In case something went wrong, we reset the stack *) - clear_tag (); - in - let logger level strm = match level with - | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm - | Info -> msg !std_ft strm - | Notice -> msg !std_ft strm - | Warning -> - let header = ("Warning", warning_tag) in - Flags.if_warn (fun () -> msg ~header !err_ft strm) () - | Error -> msg ~header:("Error", error_tag) !err_ft strm in - let () = set_logger logger in - () + pp_with ~pp_tag ft strm; + Format.pp_print_newline ft (); + Format.pp_print_flush ft (); + (** In case something went wrong, we reset the stack *) + !clear_tag_fn () diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli index 97b5869f9..1cd701ed4 100644 --- a/lib/ppstyle.mli +++ b/lib/ppstyle.mli @@ -11,7 +11,8 @@ (** {5 Style tags} *) -type t +type t = string + (** Style tags *) val make : ?style:Terminal.style -> string list -> t @@ -46,12 +47,11 @@ val dump : unit -> (t * Terminal.style option) list (** {5 Setting color output} *) val init_color_output : unit -> unit -(** Once called, all tags defined here will use their current style when - printed. To this end, this function redefines the loggers used when sending - messages to the user. The program will in particular use the formatters - {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages, - with additional syle information provided by this module. Be careful this is - not compatible with the Emacs mode! *) + +val color_msg : ?header:string * Format.tag -> + Format.formatter -> Pp.std_ppcmds -> unit +(** {!color_msg ?header fmt pp} will format according to the tags + defined in this file *) val pp_tag : Pp.tag_handler (** Returns the name of a style tag that is understandable by the formatters diff --git a/lib/system.ml b/lib/system.ml index e54109a2f..8cdcaf5dc 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -88,9 +88,9 @@ let all_subdirs ~unix_path:root = | _ -> () in process_directory f path in - check_unix_dir (fun s -> msg_warning (str s)) root; + check_unix_dir (fun s -> Feedback.msg_warning (str s)) root; if exists_dir root then traverse root [] - else msg_warning (str ("Cannot open " ^ root)); + else Feedback.msg_warning (str ("Cannot open " ^ root)); List.rev !l (* Caching directory contents for efficient syntactic equality of file @@ -149,7 +149,7 @@ let where_in_path ?(warn=true) path filename = | (lpe, f) :: l' -> let () = match l' with | _ :: _ when warn -> - msg_warning + Feedback.msg_warning (str filename ++ str " has been found in" ++ spc () ++ hov 0 (str "[ " ++ hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) @@ -205,7 +205,7 @@ let is_in_system_path filename = let lpath = CUnix.path_to_list (Sys.getenv "PATH") in is_in_path lpath filename with Not_found -> - msg_warning (str "system variable PATH not found"); + Feedback.msg_warning (str "system variable PATH not found"); false let open_trapping_failure name = @@ -216,7 +216,7 @@ let open_trapping_failure name = let try_remove filename = try Sys.remove filename with e when Errors.noncritical e -> - msg_warning + Feedback.msg_warning (str"Could not remove file " ++ str filename ++ str" which is corrupted!") let error_corrupted file s = @@ -345,13 +345,13 @@ let with_time time f x = let y = f x in let tend = get_time() in let msg2 = if time then "" else " (successful)" in - msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if time then "" else "Finished failing transaction in " in let msg2 = if time then "" else " (failure)" in - msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e let process_id () = diff --git a/library/declare.ml b/library/declare.ml index c59d190a0..b0df32b8d 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -398,7 +398,7 @@ let declare_mind mie = let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "no recursive definition") | [id] -> pr_id id ++ str " is recursively defined" ++ (match indexes with @@ -413,7 +413,7 @@ let fixpoint_message indexes l = | None -> mt ())) let cofixpoint_message l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "No corecursive definition.") | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -423,13 +423,13 @@ let recursive_message isfix i l = (if isfix then fixpoint_message i else cofixpoint_message) l let definition_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined") let assumption_message id = (* Changing "assumed" to "declared", "assuming" referring more to the type of the object than to the name of the object (see discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) - Flags.if_verbose msg_info (pr_id id ++ str " is declared") + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared") (** Global universe names, in a different summary *) diff --git a/library/goptions.ml b/library/goptions.ml index 5f6512e11..4aa3a2a21 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -108,7 +108,8 @@ module MakeTable = (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = - pp (str table_name ++ + Feedback.msg_notice + (str table_name ++ (hov 0 (if MySet.is_empty table then str " None" ++ fnl () else MySet.fold @@ -122,7 +123,7 @@ module MakeTable = method mem x = let y = A.encode x in let answer = MySet.mem y !t in - msg_info (A.member_message y answer) + Feedback.msg_info (A.member_message y answer) method print = print_table A.title A.printer !t end @@ -271,7 +272,7 @@ let declare_option cast uncast in let warn () = if depr then - msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") + Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") in let cread () = cast (read ()) in let cwrite v = warn (); write (uncast v) in @@ -346,12 +347,12 @@ let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = try set_option_value locality check_bool_value key v - with UserError (_,s) -> msg_warning s + with UserError (_,s) -> Feedback.msg_warning s let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = try set_option_value locality check_unset_value key () - with UserError (_,s) -> msg_warning s + with UserError (_,s) -> Feedback.msg_warning s let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None @@ -375,9 +376,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in diff --git a/library/libobject.ml b/library/libobject.ml index c566840e4..b12d2038a 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -133,7 +133,7 @@ let apply_dyn_fun deflt f lobj = Failure "local to_apply_dyn_fun" -> if not (!relax_flag || Hashtbl.mem missing_tab tag) then begin - Pp.msg_warning + Feedback.msg_warning (Pp.str ("Cannot find library functions for an object with tag " ^ tag ^ " (a plugin may be missing)")); Hashtbl.add missing_tab tag () diff --git a/library/library.ml b/library/library.ml index 8e2402dda..192700be7 100644 --- a/library/library.ml +++ b/library/library.ml @@ -287,7 +287,7 @@ let locate_absolute_library dir = | [] -> raise LibNotFound | [file] -> file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ + Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ str vo ++ str " because it is more recent"); vi | [vo;vi] -> vo @@ -311,7 +311,7 @@ let locate_qualified_library ?root ?(warn = true) qid = | [lpath, file] -> lpath, file | [lpath_vo, vo; lpath_vi, vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ + Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ str vo ++ str " because it is more recent"); lpath_vi, vi | [lpath_vo, vo; _ ] -> lpath_vo, vo @@ -370,7 +370,7 @@ let access_table what tables dp i = | Fetched t -> t | ToFetch f -> let dir_path = Names.DirPath.to_string dp in - Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); let t = try fetch_delayed f with Faulty f -> @@ -448,7 +448,7 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) let rec intern_library (needed, contents) (dir, f) from = - Pp.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> @@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from = (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); + Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); m.library_digests, intern_library_deps (needed, contents) dir m (Some f) and intern_library_deps libs dir m from = @@ -755,7 +755,7 @@ let save_library_to ?todo dir f otab = error "Could not compile the library to native code." with reraise -> let reraise = Errors.push reraise in - let () = msg_warning (str "Removed file " ++ str f') in + let () = Feedback.msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise diff --git a/library/loadpath.ml b/library/loadpath.ml index f8169576d..33c0f41e1 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -72,7 +72,7 @@ let add_load_path phys_path coq_path ~implicit = let () = (* Do not warn when overriding the default "-I ." path *) if not (DirPath.equal old_path Nameops.default_root_prefix) then - msg_warning + Feedback.msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath old_path ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path) in diff --git a/library/nametab.ml b/library/nametab.ml index bbae98fc0..db902d625 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -119,7 +119,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" + Feedback.msg_warning (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")); tree.path | Nothing @@ -155,7 +155,7 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" + Feedback.msg_warning (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")); tree.path | Nothing @@ -525,7 +525,7 @@ let shortest_qualid_of_tactic kn = let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> - if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e + if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e let global_inductive r = match global r with diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 451e0987b..5d3c149ab 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -1031,7 +1031,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY -| [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ] +| [ "Print" "Equivalent" "Keys" ] -> [ Feedback.msg_info (Keys.pr_keys Printer.pr_global) ] END diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 0c25481d8..308b6415d 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -231,7 +231,7 @@ GEXTEND Gram Subterm (mode, oid, pc) | IDENT "appcontext"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - msg_warning (strbrk "appcontext is deprecated"); + Feedback.msg_warning (strbrk "appcontext is deprecated"); Subterm (true,oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; @@ -334,7 +334,7 @@ let vernac_solve n info tcom b = go back to the top of the prooftree *) let p = Proof.maximal_unfocus Vernacentries.command_focus p in p,status) in - if not status then Pp.feedback Feedback.AddedAxiom + if not status then Feedback.feedback Feedback.AddedAxiom let pr_ltac_selector = function | SelectNth i -> int i ++ str ":" @@ -408,7 +408,7 @@ END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - [ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ] + [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ] END let pr_ltac_ref = Libnames.pr_reference diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4 index 4cd8bf1fe..987b9d538 100644 --- a/ltac/g_obligations.ml4 +++ b/ltac/g_obligations.ml4 @@ -121,7 +121,7 @@ open Pp VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY | [ "Show" "Obligation" "Tactic" ] -> [ - msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] + Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] END VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY @@ -130,8 +130,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ] -| [ "Preterm" ] -> [ msg_info (show_term None) ] +| [ "Preterm" "of" ident(name) ] -> [ Feedback.msg_info (show_term (Some name)) ] +| [ "Preterm" ] -> [ Feedback.msg_info (show_term None) ] END open Pp diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index 395c2cd1b..29ffbed19 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -262,5 +262,5 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Pp.msg_notice (Autorewrite.print_rewrite_hintdb s) ] + [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ] END diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index ddbd818bf..1d9e7b34e 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -435,7 +435,7 @@ let register_ltac local tacl = with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) in let () = if is_primitive then - msg_warning (str "The Ltac name " ++ id_pp ++ + Feedback.msg_warning (str "The Ltac name " ++ id_pp ++ str " may be unusable because of a conflict with a notation.") in NewTac id, body @@ -473,10 +473,10 @@ let register_ltac local tacl = let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac; - Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (Nameops.pr_id id ++ str " is defined") | UpdateTac kn -> Tacenv.redefine_ltac local kn tac; let name = Nametab.shortest_qualid_of_tactic kn in - Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined") + Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined") in List.iter iter defs diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index 39db6268b..005d1f5f4 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -54,7 +54,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = if MLTacMap.mem s !tac_tab then if overwrite then let () = tac_tab := MLTacMap.remove s !tac_tab in - msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s) + Feedback.msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s) else Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") in diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5d282a693..406fd41ad 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1242,7 +1242,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg a -> interp_tactic ist (TacArg a) | TacInfo tac -> - msg_warning + Feedback.msg_warning (strbrk "The general \"info\" tactic is currently not working." ++ spc()++ strbrk "There is an \"Info\" command to replace it." ++fnl () ++ strbrk "Some specific verbose tactics may also exist, such as info_eauto."); diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 1326818fc..3f504b7f3 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -93,7 +93,7 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (eq_constr (Universes.constr_of_global ref') t') then - msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ + Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; ref' diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 8b8b38c34..9a7aeaf0c 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -199,7 +199,7 @@ let check_keyword str = let check_keyword_to_add s = try check_keyword s with Error.E (UnsupportedUnicode unicode) -> - Flags.if_verbose msg_warning + Flags.if_verbose Feedback.msg_warning (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \ which will not be parsable." s unicode)) @@ -322,7 +322,7 @@ let rec string in_comments bp len = parser | [< '')'; s >] -> let () = match in_comments with | Some 0 -> - msg_warning + Feedback.msg_warning (strbrk "Not interpreting \"*)\" as the end of current \ non-terminated comment because it occurs in a \ @@ -389,9 +389,10 @@ let comment_stop ep = let bp = match !comment_begin with Some bp -> bp | None -> - msgerrnl(str "No begin location for comment '" - ++ str current_s ++str"' ending at " - ++ int ep); + Feedback.msg_notice + (str "No begin location for comment '" + ++ str current_s ++str"' ending at " + ++ int ep); ep-1 in Pp.comments := ((bp,ep),current_s) :: !Pp.comments); Buffer.clear current; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 1a27d9692..87e27be69 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -473,10 +473,10 @@ GEXTEND Gram [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat) | IDENT "_eqn"; ":"; pat = naming_intropattern -> let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in - msg_warning (strbrk msg); Some (!@loc, pat) + Feedback.msg_warning (strbrk msg); Some (!@loc, pat) | IDENT "_eqn" -> let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in - msg_warning (strbrk msg); Some (!@loc, IntroAnonymous) + Feedback.msg_warning (strbrk msg); Some (!@loc, IntroAnonymous) | -> None ] ] ; as_name: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index df42d9084..0df15babd 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -125,13 +125,13 @@ END let test_plural_form = function | [(_,([_],_))] -> - Flags.if_verbose msg_warning + Flags.if_verbose Feedback.msg_warning (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") | _ -> () let test_plural_form_types = function | [([_],_)] -> - Flags.if_verbose msg_warning + Flags.if_verbose Feedback.msg_warning (strbrk "Keywords Implicit Types expect more than one type") | _ -> () @@ -448,7 +448,7 @@ GEXTEND Gram VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> Flags.if_verbose - msg_warning (strbrk "Include Type is deprecated; use Include instead"); + Feedback.msg_warning (strbrk "Include Type is deprecated; use Include instead"); VernacInclude(e::l) ] ] ; export_token: @@ -667,7 +667,7 @@ GEXTEND Gram (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); + Feedback. msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); VernacArgumentsScope (qid,scl) (* Implicit *) @@ -675,7 +675,7 @@ GEXTEND Gram pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> Flags.if_verbose - msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); + Feedback.msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 898dcd255..76db2f3c2 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -25,7 +25,7 @@ let init_size=5 let cc_verbose=ref false let debug x = - if !cc_verbose then msg_debug (x ()) + if !cc_verbose then Feedback.msg_debug (x ()) let _= let gdopt= diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c8924073c..bd788a425 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -424,10 +424,10 @@ let cc_tactic depth additionnal_terms = List.map (build_term_to_complete uf newmeta) (epsilons uf) in - Pp.msg_info + Feedback.msg_info (Pp.str "Goal is solvable by congruence but \ some arguments are missing."); - Pp.msg_info + Feedback.msg_info (Pp.str " Try " ++ hov 8 begin diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index be6ce59bd..3fa600ac2 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -169,7 +169,7 @@ let do_daimon () = daimon_instr env p end in - if not status then Pp.feedback Feedback.AddedAxiom else () + if not status then Feedback.feedback Feedback.AddedAxiom else () (* post-instruction focus management *) @@ -291,7 +291,7 @@ let justification tac gls= error "Insufficient justification." else begin - msg_warning (str "Insufficient justification."); + Feedback.msg_warning (str "Insufficient justification."); daimon_tac gls end) gls @@ -1293,7 +1293,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = end; match bro with None -> - msg_warning (str "missing case"); + Feedback.msg_warning (str "missing case"); tacnext (mkMeta 1) | Some (sub_ids,tree) -> let br_args = diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 67c1c5901..a03be5743 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -541,7 +541,7 @@ let print_structure_to_file (fn,si,mo) dry struc = (if dry then None else si); (* Print the buffer content via Coq standard formatter (ok with coqide). *) if not (Int.equal (Buffer.length buf) 0) then begin - Pp.msg_notice (str (Buffer.contents buf)); + Feedback.msg_notice (str (Buffer.contents buf)); Buffer.reset buf end @@ -635,7 +635,7 @@ let simple_extraction r = in let ans = flag ++ print_one_decl struc (modpath_of_r r) d in reset (); - Pp.msg_notice ans + Feedback.msg_notice ans | _ -> assert false diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index eb2f02244..0a8cb0ccd 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -101,7 +101,7 @@ END VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY | [ "Print" "Extraction" "Inline" ] - -> [ msg_info (print_extraction_inline ()) ] + -> [Feedback. msg_info (print_extraction_inline ()) ] END VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF @@ -123,7 +123,7 @@ END VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY | [ "Print" "Extraction" "Blacklist" ] - -> [ msg_info (print_extraction_blacklist ()) ] + -> [ Feedback.msg_info (print_extraction_blacklist ()) ] END VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f336941ee..560fe5aea 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -300,7 +300,7 @@ let warning_axioms () = if List.is_empty info_axioms then () else begin let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in - msg_warning + Feedback.msg_warning (str ("The following "^s^" must be realized in the extracted code:") ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) ++ str "." ++ fnl ()) @@ -310,7 +310,7 @@ let warning_axioms () = else begin let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were" in - msg_warning + Feedback.msg_warning (str ("The following logical "^s^" encountered:") ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") @@ -326,12 +326,12 @@ let warning_opaques accessed = else let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in if accessed then - msg_warning + Feedback.msg_warning (str "The extraction is currently set to bypass opacity,\n" ++ str "the following opaque constant bodies have been accessed :" ++ lst ++ str "." ++ fnl ()) else - msg_warning + Feedback.msg_warning (str "The extraction now honors the opacity constraints by default,\n" ++ str "the following opaque constants have been extracted as axioms :" ++ lst ++ str "." ++ fnl () ++ @@ -339,7 +339,7 @@ let warning_opaques accessed = ++ fnl ()) let warning_both_mod_and_cst q mp r = - msg_warning + Feedback.msg_warning (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ str "do you mean module " ++ pr_long_mp mp ++ @@ -358,7 +358,7 @@ let check_inside_module () = err (str "You can't do that within a Module Type." ++ fnl () ++ str "Close it and try again.") else if Lib.is_module () then - msg_warning + Feedback.msg_warning (str "Extraction inside an opened module is experimental.\n" ++ str "In case of problem, close it first.\n") @@ -368,7 +368,7 @@ let check_inside_section () = str "Close it and try again.") let warning_id s = - msg_warning (str ("The identifier "^s^ + Feedback.msg_warning (str ("The identifier "^s^ " contains __ which is reserved for the extraction")) let error_constant r = @@ -449,7 +449,7 @@ let error_remaining_implicit k = let warning_remaining_implicit k = let s = msg_of_implicit k in - msg_warning + Feedback.msg_warning (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl () ++ str "but this code is potentially unsafe, please review it manually.") @@ -465,7 +465,7 @@ let check_loaded_modfile mp = match base_mp mp with | _ -> () let info_file f = - Flags.if_verbose msg_info + Flags.if_verbose Feedback.msg_info (str ("The file "^f^" has been created by extraction.")) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 134b6ba94..a78532e33 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -74,7 +74,7 @@ END VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY | [ "Print" "Firstorder" "Solver" ] -> [ - Pp.msg_info + Feedback.msg_info (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ] END @@ -131,7 +131,7 @@ ARGUMENT EXTEND firstorder_using | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] | [ "using" reference(a) reference(b) reference_list(l) ] -> [ Flags.if_verbose - Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); + Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); a::b::l ] | [ ] -> [ [] ] diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 3b9f67f66..d7da85b4f 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -32,7 +32,7 @@ let ground_tac solver startseq gl= update_flags (); let rec toptac skipped seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Pp.msg_debug (Printer.pr_goal gl); + then Feedback.msg_debug (Printer.pr_goal gl); tclORELSE (axiom_tac seq.gl seq) begin try diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 879145c2f..52094cf08 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -52,17 +52,17 @@ let rec print_debug_queue e = let _ = match e with | Some e -> - Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) | None -> begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); + Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); end in print_debug_queue None ; end let observe strm = if do_observe () - then Pp.msg_debug strm + then Feedback.msg_debug strm else () let do_observe_tac s tac g = diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 91a826c73..5b4fb2595 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -19,7 +19,7 @@ exception Toberemoved let observe s = if do_observe () - then Pp.msg_debug s + then Feedback.msg_debug s (* Transform an inductive induction principle into diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6dfc23511..c63527dea 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -193,12 +193,12 @@ let warning_error names e = let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - Pp.msg_warning + Feedback.msg_warning (str "Cannot define graph(s) for " ++ h 1 (pr_enum Libnames.pr_reference names) ++ if do_observe () then (spc () ++ Errors.print e) else mt ()) | Defining_principle e -> - Pp.msg_warning + Feedback.msg_warning (str "Cannot define principle(s) for "++ h 1 (pr_enum Libnames.pr_reference names) ++ if do_observe () then Errors.print e else mt ()) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8a0a1a064..72205e2bb 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -14,7 +14,7 @@ open Misctypes let observe strm = if do_observe () - then Pp.msg_debug strm + then Feedback.msg_debug strm else () (*let observennl strm = if do_observe () diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 84a4d910e..0cacb003d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -267,12 +267,12 @@ let derive_inversion fix_names = lind; with e when Errors.noncritical e -> let e' = process_vernac_interp_error e in - msg_warning + Feedback.msg_warning (str "Cannot build inversion information" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) with e when Errors.noncritical e -> let e' = process_vernac_interp_error e in - msg_warning + Feedback.msg_warning (str "Cannot build inversion information (early)" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) @@ -292,12 +292,12 @@ let warning_error names e = in match e with | Building_graph e -> - Pp.msg_warning + Feedback.msg_warning (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) | Defining_principle e -> - Pp.msg_warning + Feedback.msg_warning (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 72529fbbe..94530bfde 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -53,7 +53,7 @@ let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = let observe strm = if do_observe () - then Pp.msg_debug strm + then Feedback.msg_debug strm else () (*let observennl strm = diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index c71d9a9ca..99a165044 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -504,19 +504,19 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> - let _ = prstr "\nICI1!\n";Pp.flush_all() in + let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args) | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge | GLetIn(_,nme,bdy,trm) , _ -> - let _ = prstr "\nICI2!\n";Pp.flush_all() in + let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in GLetIn(Loc.ghost,nme,bdy,newtrm) | _, GLetIn(_,nme,bdy,trm) -> - let _ = prstr "\nICI3!\n";Pp.flush_all() in + let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in GLetIn(Loc.ghost,nme,bdy,newtrm) - | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in + | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge let rec merge_app_unsafe c1 c2 shift filter_shift_stable = @@ -527,14 +527,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) | GLetIn(_,nme,bdy,trm) , _ -> - let _ = prstr "\nICI2 '!\n";Pp.flush_all() in + let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in GLetIn(Loc.ghost,nme,bdy,newtrm) | _, GLetIn(_,nme,bdy,trm) -> - let _ = prstr "\nICI3 '!\n";Pp.flush_all() in + let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in GLetIn(Loc.ghost,nme,bdy,newtrm) - | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge + | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 10f08d3d1..80866e8b8 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -214,17 +214,17 @@ let print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) else begin - Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); + Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); end; (* print_debug_queue false e; *) end let observe strm = if do_observe () - then Pp.msg_debug strm + then Feedback.msg_debug strm else () @@ -1537,7 +1537,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num with e when Errors.noncritical e -> begin if do_observe () - then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e) + then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e) else anomaly (Pp.str "Cannot create equation Lemma") ; true diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 0fcfbfc71..e4aa1448e 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -961,7 +961,7 @@ struct let parse_expr parse_constant parse_exp ops_spec env term = if debug - then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term); + then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term); (* let constant_or_variable env term = @@ -1082,7 +1082,7 @@ struct let rconstant term = if debug - then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ()); + then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ()); let res = rconstant term in if debug then (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; @@ -1122,7 +1122,7 @@ struct let parse_arith parse_op parse_expr env cstr gl = if debug - then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ()); + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ()); match kind_of_term cstr with | App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in @@ -1651,12 +1651,12 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 if debug then begin - Pp.pp (Pp.str "Formula....\n") ; + Feedback.msg_notice (Pp.str "Formula....\n") ; let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in - Pp.pp (Printer.prterm ff) ; Pp.pp_flush (); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff + Feedback.msg_notice (Printer.prterm ff); + Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff end; match witness_list_tags prover cnf_ff with @@ -1676,11 +1676,11 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 if debug then begin - Pp.pp (Pp.str "\nAFormula\n") ; + Feedback.msg_notice (Pp.str "\nAFormula\n") ; let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff' in - Pp.pp (Printer.prterm ff') ; Pp.pp_flush (); + Feedback.msg_notice (Printer.prterm ff'); Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' end; @@ -1733,7 +1733,7 @@ let micromega_gen with | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") - | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; + | CsdpNotFound -> flush stdout ; Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " ^ "the use of a specialized external tool called csdp. \n\n" @@ -1818,7 +1818,7 @@ let micromega_genr prover = with | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut") | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") - | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; + | CsdpNotFound -> Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " ^ "the use of a specialized external tool called csdp. \n\n" @@ -1903,7 +1903,7 @@ let call_csdpcert_q provername poly = let cert = Certificate.q_cert_of_pos cert in if Mc.qWeakChecker poly cert then Some cert - else ((print_string "buggy certificate" ; flush stdout) ;None) + else ((print_string "buggy certificate") ;None) let call_csdpcert_z provername poly = let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index dca46cbcf..007a9ec67 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -172,7 +172,7 @@ let print_env_reification env = 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) + Feedback.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/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 3ba92b9f2..f3eae5f50 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -547,7 +547,7 @@ let pp_info () = int s_info.created_branches ++ str " created" ++ fnl () ++ str "Hypotheses : " ++ int s_info.created_hyps ++ str " created" ++ fnl () in - msg_info + Feedback.msg_info ( str "Proof-search statistics :" ++ fnl () ++ count_info ++ str "Branch ends: " ++ diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 73dc13e72..0a0b45915 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -276,7 +276,7 @@ let rtauto_tac gls= begin reset_info (); if !verbose then - msg_info (str "Starting proof-search ..."); + Feedback.msg_info (str "Starting proof-search ..."); end in let search_start_time = System.get_time () in let prf = @@ -286,10 +286,10 @@ let rtauto_tac gls= let search_end_time = System.get_time () in let _ = if !verbose then begin - msg_info (str "Proof tree found in " ++ + Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); pp_info (); - msg_info (str "Building proof term ... ") + Feedback.msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in let _ = step_count := 0; node_count := 0 in @@ -302,7 +302,7 @@ let rtauto_tac gls= let build_end_time=System.get_time () in let _ = if !verbose then begin - msg_info (str "Proof term built in " ++ + Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ fnl () ++ str "Proof size : " ++ int !step_count ++ @@ -319,9 +319,9 @@ let rtauto_tac gls= Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in let _ = - if !check then msg_info (str "Proof term type-checking is on"); + if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then - msg_info (str "Internal tactic executed in " ++ + Feedback.msg_info (str "Internal tactic executed in " ++ System.fmt_time_difference tac_start_time tac_end_time) in result diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index f5a734048..f64226e33 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -60,9 +60,9 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in add_theory id (ic t) set k cst (pre,post) power sign div] | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following ring structures have been declared:"); + Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> - msg_notice (hov 2 + Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr fi.ring_carrier++spc()++ str"and equivalence relation "++ pr_constr fi.ring_req)) @@ -89,9 +89,9 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following field structures have been declared:"); + Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> - msg_notice (hov 2 + Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr fi.field_carrier++spc()++ str"and equivalence relation "++ pr_constr fi.field_req)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 271bf35a8..154ec6e1b 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -527,7 +527,7 @@ let ring_equality env evd (r,add,mul,opp,req) = let op_morph = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose - msg_info + Feedback.msg_info (str"Using setoid \""++pr_constr req++str"\""++spc()++ str"and morphisms \""++pr_constr add_m_lem ++ str"\","++spc()++ str"\""++pr_constr mul_m_lem++ @@ -536,7 +536,7 @@ let ring_equality env evd (r,add,mul,opp,req) = op_morph) | None -> (Flags.if_verbose - msg_info + Feedback.msg_info (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ str"and morphisms \""++pr_constr add_m_lem ++ str"\""++spc()++str"and \""++ diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 5f44904c3..fe9386039 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -25,7 +25,7 @@ let threshold = of_int 5000 let nat_of_int dloc n = if is_pos_or_zero n then begin if less_than threshold n then - msg_warning + Feedback.msg_warning (strbrk "Stack overflow or segmentation fault happens when " ++ strbrk "working with large numbers in nat (observed threshold " ++ strbrk "may vary from 5000 to 70000 depending on your system " ++ diff --git a/pretyping/classops.ml b/pretyping/classops.ml index ece92b66b..55220f44c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && is_verbose () then - msg_warning (message_ambig !ambig_paths) + Feedback.msg_warning (message_ambig !ambig_paths) type coercion = { coercion_type : coe_typ; diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 4fb411202..129725c6d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -50,11 +50,11 @@ type bound_ident_map = Id.t Id.Map.t exception PatternMatchingFailure let warn_bound_meta name = - msg_warning (str "Collision between bound variable " ++ pr_id name ++ + Feedback.msg_warning (str "Collision between bound variable " ++ pr_id name ++ str " and a metavariable of same name.") let warn_bound_bound name = - msg_warning (str "Collision between bound variables of name " ++ pr_id name) + Feedback.msg_warning (str "Collision between bound variables of name " ++ pr_id name) let constrain n (ids, m as x) (names, terms as subst) = try diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c973e1cef..86921c49b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -620,7 +620,7 @@ and share_names flags n l avoid env sigma c t = share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then msg_warning (strbrk "Detyping.detype: cannot factorize fix enough"); + if n>0 then Feedback.msg_warning (strbrk "Detyping.detype: cannot factorize fix enough"); let c = detype flags avoid env sigma c in let t = detype flags avoid env sigma t in (List.rev l,c,t) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 08973a05c..89cb723bc 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -501,7 +501,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) + Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index e3b6fb08a..04100c8a7 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -336,8 +336,8 @@ let glob_visible_short_qualid c = let add_and_check_ident id set = if Id.Set.mem id set then - Pp.(msg_warning - (str "Collision between bound variables of name " ++ Id.print id)); + Feedback.msg_warning + Pp.(str "Collision between bound variables of name " ++ Id.print id); Id.Set.add id set let bound_glob_vars = diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 8b061e3c2..5d36fc78e 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -184,7 +184,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = (match dest_recarg ra with | Mrec (_,j) when is_rec -> (depPvect.(j),rest) | Imbr _ -> - msg_warning (strbrk "Ignoring recursive call"); + Feedback.msg_warning (strbrk "Ignoring recursive call"); (None,rest) | _ -> (None, rest)) in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 17bf28793..2a5e99965 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -389,16 +389,16 @@ let native_norm env sigma c ty = let code, upd = mk_norm_code penv sigma prefix c in match Nativelib.compile ml_filename code with | true, fn -> - if !Flags.debug then Pp.msg_debug (Pp.str "Running norm ..."); + if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); let t0 = Sys.time () in Nativelib.call_linker ~fatal:true prefix fn (Some upd); let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Pp.msg_debug (Pp.str time_info); + if !Flags.debug then Feedback.msg_debug (Pp.str time_info); let res = nf_val env !Nativelib.rt1 ty in let t2 = Sys.time () in let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in - if !Flags.debug then Pp.msg_debug (Pp.str time_info); + if !Flags.debug then Feedback.msg_debug (Pp.str time_info); res | _ -> anomaly (Pp.str "Compilation failure") diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 827071054..d6305d81a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -348,7 +348,7 @@ let rec pat_of_raw metas vars = function | GHole _ -> PMeta None | GCast (_,c,_) -> - Pp.msg_warning (strbrk "Cast not taken into account in constr pattern"); + Feedback.msg_warning (strbrk "Cast not taken into account in constr pattern"); pat_of_raw metas vars c | GIf (_,c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 6499ddd53..bbb6a9266 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -216,7 +216,7 @@ let compute_canonical_projections (con,ind) = if Flags.is_verbose () then (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - msg_warning (strbrk "No global reference exists for projection value" + Feedback.msg_warning (strbrk "No global reference exists for projection value" ++ Termops.print_constr t ++ strbrk " in instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")); l @@ -250,7 +250,7 @@ let open_canonical_structure i (_,o) = and new_can_s = (Termops.print_constr s.o_DEF) in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in - msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val + Feedback.msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val ++ strbrk " by " ++ prj ++ strbrk " in " ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b6eb3a037..79cb7a2f6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -802,14 +802,15 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let rec whrec cst_l (x, stack as s) = let () = if !debug_RAKAM then let open Pp in - pp (h 0 (str "<<" ++ Termops.print_constr x ++ + Feedback.msg_notice + (h 0 (str "<<" ++ Termops.print_constr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++ str ">>") ++ fnl ()) in let fold () = let () = if !debug_RAKAM then - let open Pp in pp (str "<><><><><>" ++ fnl ()) in + let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in (s,cst_l) in match kind_of_term x with diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a4a386530..cdd543d25 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -657,7 +657,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb and cN = Evarutil.whd_head_evar sigma curn in let () = if !debug_unification then - msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN) + Feedback.msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN) in match (kind_of_term cM,kind_of_term cN) with | Meta k1, Meta k2 -> @@ -1054,7 +1054,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb else error_cannot_unify (fst curenvnb) sigma (cM,cN) in - if !debug_unification then msg_debug (str "Starting unification"); + if !debug_unification then Feedback.msg_debug (str "Starting unification"); let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in try let res = @@ -1075,10 +1075,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let a = match res with | Some sigma -> sigma, ms, es | None -> unirec_rec (env,0) cv_pb opt subst m n in - if !debug_unification then msg_debug (str "Leaving unification with success"); + if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> - if !debug_unification then msg_debug (str "Leaving unification with failure"); + if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); raise e diff --git a/printing/printer.ml b/printing/printer.ml index cb075c64f..a43ccff46 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -551,7 +551,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals (* Side effect! This has to be made more robust *) let () = match close_cmd with - | Some cmd -> msg_info cmd + | Some cmd -> Feedback.msg_info cmd | None -> () in match goals with @@ -629,12 +629,12 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = begin match bgoals,shelf,given_up with | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals | [] , [] , _ -> - msg_info (str "No more subgoals, but there are some goals you gave up:"); + Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> - msg_info (str "All the remaining goals are on the shelf."); + Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 5367a907e..45af036fb 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -111,7 +111,7 @@ let solve ?with_end_tac gi info_lvl tac pr = let () = match info_lvl with | None -> () - | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) + | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) in (p,status) with diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index 681a7fa1a..caa9b328a 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -128,7 +128,7 @@ let suggest_Proof_using name env vars ids_typ context_ids = if S.equal all_needed fwd_typ then valid (str "Type*"); if S.equal all all_needed then valid(str "All"); valid (pr_set false needed); - msg_info ( + Feedback.msg_info ( str"The proof of "++ str name ++ spc() ++ str "should start with one of the following commands:"++spc()++ v 0 ( diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 2d886b8e1..13b5848a3 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -31,7 +31,7 @@ let cbv_vm env sigma c = let cbv_native env sigma c = if Coq_config.no_native_compiler then - let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in + let () = Feedback.msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in cbv_vm env sigma c else let ctyp = Retyping.get_type_of env sigma c in @@ -221,7 +221,7 @@ let reduction_of_red_expr env = let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in let () = if not (!simplIsCbn || List.is_empty f.rConst) then - Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in + Feedback.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) | Cbn f -> diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 186525e15..23433692c 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -57,7 +57,7 @@ let tclIDTAC gls = goal_goal_list gls (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls + Feedback.msg_info (hov 0 s); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) @@ -218,7 +218,8 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in - pp (str (emacs_str "") + Feedback.msg_notice + (str (emacs_str "") ++ (hov 0 (str s)) ++ (str (emacs_str "")) ++ fnl()); tclIDTAC goal;; diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index c7faef333..0ca4d6020 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -104,7 +104,8 @@ module Make(T : Task) = struct marshal_err ("unmarshal_more_data: "^s) let report_status ?(id = !Flags.async_proofs_worker_id) s = - Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s)) + let open Feedback in + feedback ~id:(State Stateid.initial) (WorkerStatus(id, s)) module Worker = Spawn.Sync(struct end) @@ -302,8 +303,8 @@ module Make(T : Task) = struct let main_loop () = let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback fb) []; flush oc in - Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); - Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg)); + Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); + Feedback.set_logger Feedback.feedback_logger; Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with diff --git a/stm/lemmas.ml b/stm/lemmas.ml index ce5ef0169..afbc407d8 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -150,7 +150,7 @@ let find_mutually_recursive_statements thms = assert (List.is_empty rest); (* One occ. of common coind ccls and no common inductive hyps *) if not (List.is_empty common_same_indhyp) then - if_verbose msg_info (str "Assuming mutual coinductive statements."); + if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); flush_all (); indccl, true, [] | [], _::_ -> @@ -158,7 +158,7 @@ let find_mutually_recursive_statements thms = | ind :: _ -> if List.distinct_f ind_ord (List.map pi1 ind) then - if_verbose msg_info + if_verbose Feedback.msg_info (strbrk ("Coinductive statements do not follow the order of "^ "definition, assuming the proof to be by induction.")); @@ -306,7 +306,7 @@ let admit (id,k,e) pl hook () = let () = match k with | Global, _, _ -> () | Local, _, _ | Discharge, _, _ -> - msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ + Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ str "declared as an axiom.") in let () = assumption_message id in @@ -336,7 +336,7 @@ let universe_proof_terminator compute_guard hook = make_terminator begin function | Admitted (id,k,pe,(ctx,pl)) -> admit (id,k,pe) pl (hook (Some ctx)) (); - Pp.feedback Feedback.AddedAxiom + Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff, exports = match opaque with | Vernacexpr.Transparent -> false, true, [] diff --git a/stm/stm.ml b/stm/stm.ml index 8f11875b6..28e749d5c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -18,6 +18,7 @@ open Names open Util open Ppvernac open Vernac_classifier +open Feedback module Hooks = struct @@ -27,28 +28,23 @@ let with_fail, with_fail_hook = Hook.make () let state_computed, state_computed_hook = Hook.make ~default:(fun state_id ~in_cache -> - feedback ~state_id Feedback.Processed) () + feedback ~id:(State state_id) Processed) () let state_ready, state_ready_hook = Hook.make ~default:(fun state_id -> ()) () let forward_feedback, forward_feedback_hook = Hook.make ~default:(function - | { Feedback.id = Feedback.Edit edit_id; route; contents } -> - feedback ~edit_id ~route contents - | { Feedback.id = Feedback.State state_id; route; contents } -> - feedback ~state_id ~route contents) () + | { id = id; route; contents } -> + feedback ~id:id ~route contents) () let parse_error, parse_error_hook = Hook.make - ~default:(function - | Feedback.Edit edit_id -> fun loc msg -> - feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg)) - | Feedback.State state_id -> fun loc msg -> - feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) () + ~default:(fun id loc msg -> + feedback ~id (ErrorMsg (loc, Pp.string_of_ppcmds msg))) () let execution_error, execution_error_hook = Hook.make ~default:(fun state_id loc msg -> - feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) () + feedback ~id:(State state_id) (ErrorMsg (loc, Pp.string_of_ppcmds msg))) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -106,11 +102,11 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e | _ -> false in if internal_command expr then begin - prerr_endline (fun () -> "ignoring " ^ string_of_ppcmds(pr_vernac expr)) + prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) end else begin - set_id_for_feedback ?route (Feedback.State id); + set_id_for_feedback ?route (State id); Aux_file.record_in_aux_set_at loc; - prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr)); + prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) with e -> let e = Errors.push e in @@ -120,8 +116,8 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = (* Wrapper for Vernac.parse_sentence to set the feedback id *) let vernac_parse ?newtip ?route eid s = let feedback_id = - if Option.is_empty newtip then Feedback.Edit eid - else Feedback.State (Option.get newtip) in + if Option.is_empty newtip then Edit eid + else State (Option.get newtip) in set_id_for_feedback ?route feedback_id; let pa = Pcoq.Gram.parsable (Stream.of_string s) in Flags.with_option Flags.we_are_parsing (fun () -> @@ -138,7 +134,7 @@ let vernac_parse ?newtip ?route eid s = let pr_open_cur_subgoals () = try Printer.pr_open_subgoals () - with Proof_global.NoCurrentProof -> str"" + with Proof_global.NoCurrentProof -> Pp.str "" let update_global_env () = if Proof_global.there_are_pending_proofs () then @@ -230,7 +226,7 @@ end = struct (* {{{ *) let find_proof_at_depth vcs pl = try List.find (function | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl - | _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth") + | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth") | _ -> false) (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs)) with Not_found -> failwith "find_proof_at_depth" @@ -238,9 +234,9 @@ end = struct (* {{{ *) exception Expired let visit vcs id = if Stateid.equal id Stateid.initial then - anomaly(str"Visiting the initial state id") + anomaly(Pp.str "Visiting the initial state id") else if Stateid.equal id Stateid.dummy then - anomaly(str"Visiting the dummy state id") + anomaly(Pp.str "Visiting the dummy state id") else try match Vcs_.Dag.from_node (Vcs_.dag vcs) id with @@ -256,7 +252,7 @@ end = struct (* {{{ *) | [n, Sideff (Some x); p, Noop] | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n } | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n} - | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id)) + | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id)) with Not_found -> raise Expired end (* }}} *) @@ -339,10 +335,10 @@ end = struct (* {{{ *) "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in let string_of_transaction = function | Cmd { cast = t } | Fork (t, _,_,_) -> - (try string_of_ppcmds (pr_ast t) with _ -> "ERR") + (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff (Some t) -> sprintf "Sideff(%s)" - (try string_of_ppcmds (pr_ast t) with _ -> "ERR") + (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff None -> "EnvChange" | Noop -> " " | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id) @@ -740,7 +736,7 @@ end = struct (* {{{ *) let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id = - feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id); + feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id); let str_id = Stateid.to_string id in if is_cached id && not redefine then anomaly (str"defining state "++str str_id++str" twice"); @@ -1062,7 +1058,7 @@ end = struct (* {{{ *) List.iter (fun (id,s) -> State.assign id s) l; `End | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop }, RespBuiltProof (pl, time) -> - feedback (Feedback.InProgress ~-1); + feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time t_name t_loc time; if !Flags.async_proofs_full || t_drop @@ -1070,7 +1066,7 @@ end = struct (* {{{ *) else `End | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> - feedback (Feedback.InProgress ~-1); + feedback (InProgress ~-1); let info = Stateid.add ~valid Exninfo.null e_error_at in let e = (RemoteException e_msg, info) in t_assign (`Exn e); @@ -1086,7 +1082,7 @@ end = struct (* {{{ *) let e = (RemoteException (strbrk s), info) in t_assign (`Exn e); Hooks.(call execution_error start Loc.ghost (strbrk s)); - feedback (Feedback.InProgress ~-1) + feedback (InProgress ~-1) let build_proof_here ~drop_pt (id,valid) loc eop = Future.create (State.exn_on id ~valid) (fun () -> @@ -1097,7 +1093,7 @@ end = struct (* {{{ *) Aux_file.record_in_aux_at loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); let p = Proof_global.return_proof ~allow_partial:drop_pt () in - if drop_pt then Pp.feedback ~state_id:id Feedback.Complete; + if drop_pt then feedback ~id:(State id) Complete; p) let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states = @@ -1190,7 +1186,7 @@ end = struct (* {{{ *) "The system state could not be sent to the worker process. "^ "Falling back to local, lazy, evaluation.")); t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop)); - feedback (Feedback.InProgress ~-1) + feedback (InProgress ~-1) end (* }}} *) @@ -1270,7 +1266,7 @@ end = struct (* {{{ *) let (e, info) = Errors.push e in (try match Stateid.get info with | None -> - pperrnl ( + msg_error ( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) | Some (_, cur) -> @@ -1280,12 +1276,12 @@ end = struct (* {{{ *) | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (`Ast ( { loc }, _)) } -> let start, stop = Loc.unloc loc in - pperrnl ( + msg_error ( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ str ": chars " ++ int start ++ str "-" ++ int stop ++ spc () ++ iprint (e, info)) | _ -> - pperrnl ( + msg_error ( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) with e -> @@ -1378,7 +1374,7 @@ end = struct (* {{{ *) else let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in - feedback (Feedback.InProgress 1); + feedback (InProgress 1); let task = ProofTask.(BuildProof { t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt; t_loc = loc; t_uuid; t_name = pname; @@ -1625,11 +1621,11 @@ end = struct (* {{{ *) Reach.known_state ~cache:`No r_where; try vernac_interp r_for { r_what with verbose = true }; - feedback ~state_id:r_for Feedback.Processed + feedback ~id:(State r_for) Processed with e when Errors.noncritical e -> let e = Errors.push e in let msg = string_of_ppcmds (iprint e) in - feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg)) + feedback ~id:(State r_for) (ErrorMsg (Loc.ghost, msg)) let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what) @@ -1897,7 +1893,7 @@ let known_state ?(redefine_qed=false) ~cache id = if not delegate then ignore(Future.compute fp); reach view.next; vernac_interp id ~proof x; - feedback ~state_id:id Feedback.Incomplete + feedback ~id:(State id) Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () @@ -2034,7 +2030,6 @@ let check_task name (tasks,rcbackup) i = let vcs = VCS.backup () in try let rc = Future.purify (Slaves.check_task name tasks) i in - pperr_flush (); VCS.restore vcs; rc with e when Errors.noncritical e -> VCS.restore vcs; false @@ -2044,7 +2039,6 @@ let finish_tasks name u d p (t,rcbackup as tasks) = let finish_task u (_,_,i) = let vcs = VCS.backup () in let u = Future.purify (Slaves.finish_task name u d p t) i in - pperr_flush (); VCS.restore vcs; u in try @@ -2052,7 +2046,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = (u,a,true), p with e -> let e = Errors.push e in - pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); + msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 let merge_proof_branch ?valid ?id qast keep brname = @@ -2357,7 +2351,7 @@ type focus = { tip : Stateid.t } -let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s = +let query ~at ?(report_with=(Stateid.dummy,default_route)) s = Future.purify (fun s -> if Stateid.equal at Stateid.dummy then finish () else Reach.known_state ~cache:`Yes at; diff --git a/tactics/auto.ml b/tactics/auto.ml index 6b58baa99..e57b48e9e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -229,11 +229,11 @@ let tclLOG (dbg,depth,trace) pp tac = Proofview.V82.tactic begin fun gl -> try let out = Proofview.V82.of_tactic tac gl in - msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); + Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); out with reraise -> let reraise = Errors.push reraise in - msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); + Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); iraise reraise end | Info -> @@ -289,10 +289,10 @@ let tclTRY_dbg d tac = let delay f = Proofview.tclUNIT () >>= fun () -> f () in let tac = match level with | Off -> tac - | Debug | Info -> delay (fun () -> msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac) + | Debug | Info -> delay (fun () -> Feedback.msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac) in let after = match level with - | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ()) + | Info -> delay (fun () -> Feedback.msg_debug (pr_info_nop d); Proofview.tclUNIT ()) | Off | Debug -> Proofview.tclUNIT () in Tacticals.New.tclORELSE0 tac after diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index cfbcc4750..95b26c2d5 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -455,7 +455,7 @@ let hints_tac hints = | None -> aux i foundone tl | Some {it = gls; sigma = s';} -> if !typeclasses_debug then - msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp + Feedback.msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp ++ str" on" ++ spc () ++ pr_ev s gl); let sgls = evars_to_goals @@ -504,7 +504,7 @@ let hints_tac hints = in let e' = match foundone with None -> e | Some e' -> merge_failures e e' in if !typeclasses_debug then - msg_debug + Feedback.msg_debug ((if do_backtrack then str"Backtracking after " else str "Not backtracking after ") ++ Lazy.force pp); @@ -514,7 +514,7 @@ let hints_tac hints = sk glsv fk') | [] -> if foundone == None && !typeclasses_debug then - msg_debug (pr_depth info.auto_depth ++ str": no match for " ++ + Feedback.msg_debug (pr_depth info.auto_depth ++ str": no match for " ++ Printer.pr_constr_env (Goal.V82.env s gl) s concl ++ spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities"); match foundone with diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f0f408c24..2cae9b794 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -344,13 +344,13 @@ let mk_eauto_dbg d = else Off let pr_info_nop = function - | Info -> msg_debug (str "idtac.") + | Info -> Feedback.msg_debug (str "idtac.") | _ -> () let pr_dbg_header = function | Off -> () - | Debug -> msg_debug (str "(* debug eauto : *)") - | Info -> msg_debug (str "(* info eauto : *)") + | Debug -> Feedback.msg_debug (str "(* debug eauto : *)") + | Info -> Feedback.msg_debug (str "(* info eauto : *)") let pr_info dbg s = if dbg != Info then () @@ -361,7 +361,7 @@ let pr_info dbg s = | State sp -> let mindepth = loop sp in let indent = String.make (mindepth - sp.depth) ' ' in - msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); + Feedback.msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); mindepth in ignore (loop s) diff --git a/tactics/hints.ml b/tactics/hints.ml index b2104ba43..b543b564c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -692,7 +692,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, else begin if not eapply then failwith "make_apply_entry"; if verbose then - msg_warning (str "the hint: eapply " ++ pr_lconstr c ++ + Feedback.msg_warning (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); (Some hd, { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); @@ -1336,7 +1336,7 @@ let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true let warn h x = let hint = pr_hint h in let (mp, _, _) = KerName.repr h.uid in - let () = msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in + let () = Feedback.msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in Proofview.tclUNIT x let run_hint tac k = match !warn_hint with diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 15e9d3a94..a2431f6ef 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1307,7 +1307,7 @@ let enforce_prop_bound_names rename tac = mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t') | LetIn (na,c,t,t') -> mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t') - | _ -> print_int i; Pp.msg (print_constr t); assert false in + | _ -> print_int i; Feedback.msg_notice (print_constr t); assert false in let rename_branch i = Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in @@ -2939,7 +2939,7 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] let check_unused_names names = if not (List.is_empty names) && Flags.is_verbose () then - msg_warning + Feedback.msg_warning (str"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 13705edaa..9886b263c 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -502,7 +502,7 @@ let coqdep () = let user = coqlib//"user-contrib" in if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user []; List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) - (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x))); + (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x))); List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; @@ -527,4 +527,4 @@ let _ = coqdep () with Errors.UserError(s,p) -> let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in - Pp.msgerrnl pp + Feedback.msg_error pp diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index e81f4038d..d5ef807b6 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -36,10 +36,10 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop = Xml_printer.print coqtop.xml_printer xml_query; let rec loop () = let xml = Xml_parser.parse coqtop.xml_parser in - if Pp.is_message xml then - let message = Pp.to_message xml in - let level = message.Pp.message_level in - let content = message.Pp.message_content in + if Feedback.is_message xml then + let message = Feedback.to_message xml in + let level = message.Feedback.message_level in + let content = message.Feedback.message_content in logger level content; loop () else if Feedback.is_feedback xml then diff --git a/toplevel/class.ml b/toplevel/class.ml index a9c53b4d4..10e9b30be 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -262,7 +262,7 @@ let add_new_coercion_core coef stre poly source target isid = in check_source (Some cls); if not (uniform_cond (llp-ind) lvs) then - msg_warning (explain_coercion_error coef NotUniform); + Feedback.msg_warning (explain_coercion_error coef NotUniform); let clt = try get_target tg ind @@ -310,7 +310,7 @@ let add_coercion_hook poly local ref = in let () = try_add_new_coercion ref stre poly in let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in - Flags.if_verbose msg_info msg + Flags.if_verbose Feedback.msg_info msg let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) diff --git a/toplevel/command.ml b/toplevel/command.ml index 5865fec06..f0f678e08 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -119,7 +119,7 @@ let interp_definition pl bl p red_option c ctypopt = impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) in if not (try List.for_all chk imps2 with Not_found -> false) - then msg_warning + then Feedback.msg_warning (strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here."); let vars = Univ.LSet.union (Universes.universes_of_constr body) @@ -140,7 +140,7 @@ let get_locality id = function | Discharge -> (** If a Let is defined outside a section, then we consider it as a local definition *) let msg = pr_id id ++ strbrk " is declared as a local definition" in - let () = msg_warning msg in + let () = Feedback.msg_warning msg in true | Local -> true | Global -> false @@ -171,7 +171,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = let () = if Pfedit.refining () then let msg = strbrk "Section definition " ++ pr_id ident ++ strbrk " is not visible from current goals" in - msg_warning msg + Feedback.msg_warning msg in gr | Discharge | Local | Global -> @@ -217,7 +217,7 @@ match local with let () = assumption_message ident in let () = if is_verbose () && Pfedit.refining () then - msg_warning (str"Variable" ++ spc () ++ pr_id ident ++ + Feedback.msg_warning (str"Variable" ++ spc () ++ pr_id ident ++ strbrk " is not visible from current goals") in let r = VarRef ident in @@ -706,7 +706,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls = constrimpls) impls; let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in - if_verbose msg_info (minductive_message warn_prim names); + if_verbose Feedback.msg_info (minductive_message warn_prim names); if mie.mind_entry_private == None then declare_default_schemes mind; mind @@ -799,7 +799,7 @@ let check_mutuality env isfix fixl = let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with | (x,Inr xge)::(y,Inr yge)::rest -> - msg_warning (non_full_mutual_message x xge y yge isfix rest) + Feedback.msg_warning (non_full_mutual_message x xge y yge isfix rest) | _ -> () type structured_fixpoint_expr = { diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index b81c8da71..e4975fa31 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -36,7 +36,7 @@ let load_rcfile() = else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try - let warn x = msg_warning (str x) in + let warn x = Feedback.msg_warning (str x) in let inferedrc = List.find CUnix.file_readable_p [ Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version; Envars.xdg_config_home warn / rcdefaultname; @@ -52,10 +52,10 @@ let load_rcfile() = *) with reraise -> let reraise = Errors.push reraise in - let () = msg_info (str"Load of rcfile failed.") in + let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise else - Flags.if_verbose msg_info (str"Skipping rcfile loading.") + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.") (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = @@ -78,7 +78,7 @@ let push_ml_include s = ml_includes := s :: !ml_includes let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in - let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in + let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in let coqpath = Envars.coqpath in let coq_root = Names.DirPath.make [Nameops.coq_root] in (* NOTE: These directories are searched from last to first *) @@ -135,6 +135,6 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - msg_warning (str "Compatibility with version " ++ str s ++ str " not supported."); + Feedback.msg_warning (str "Compatibility with version " ++ str s ++ str " not supported."); Flags.V8_2 | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".") diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 040c33924..c8879963e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -13,6 +13,8 @@ open Flags open Vernac open Pcoq +let top_stderr x = msg_with !Pp_control.err_ft x + (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -59,7 +61,7 @@ let prompt_char ic ibuf count = | ll::_ -> Int.equal ibuf.len ll | [] -> Int.equal ibuf.len 0 in - if bol && not !print_emacs then msgerr (str (ibuf.prompt())); + if bol && not !print_emacs then top_stderr (str (ibuf.prompt())); try let c = input_char ic in if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols; @@ -310,23 +312,23 @@ let read_sentence () = *) let do_vernac () = - msgerrnl (mt ()); - if !print_emacs then msgerr (str (top_buffer.prompt())); + top_stderr (fnl()); + if !print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try Vernac.eval_expr (read_sentence ()) with | End_of_input | Errors.Quit -> - msgerrnl (mt ()); pp_flush(); raise Errors.Quit + top_stderr (fnl ()); raise Errors.Quit | Errors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise Errors.Drop - else ppnl (str"Error: There is no ML toplevel." ++ fnl ()) + else Feedback.msg_error (str"There is no ML toplevel.") | any -> let any = Errors.push any in Format.set_formatter_out_channel stdout; let msg = print_toplevel_error any ++ fnl () in pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg; - pp_flush () + flush_all () (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -354,7 +356,7 @@ let rec loop () = | Errors.Drop -> () | Errors.Quit -> exit 0 | any -> - msgerrnl (str"Anomaly: main loop exited with exception: " ++ + Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++ str (Printexc.to_string any) ++ fnl() ++ str"Please report."); loop () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c4222b330..869f6bb93 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -31,10 +31,10 @@ let get_version_date () = let print_header () = let (ver,rev) = get_version_date () in - ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); - pp_flush () + Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); + flush_all () -let warning s = with_option Flags.warn msg_warning (strbrk s) +let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s) let toploop = ref None @@ -61,7 +61,8 @@ let init_color () = match colors with | None -> (** Default colors *) - Ppstyle.init_color_output () + Ppstyle.init_color_output (); + Feedback.set_logger Feedback.color_terminal_logger | Some "" -> (** No color output *) () @@ -69,7 +70,8 @@ let init_color () = (** Overwrite all colors *) Ppstyle.clear_styles (); Ppstyle.parse_config s; - Ppstyle.init_color_output () + Ppstyle.init_color_output (); + Feedback.set_logger Feedback.color_terminal_logger end let toploop_init = ref begin fun x -> @@ -95,8 +97,8 @@ let memory_stat = ref false let print_memory_stat () = begin (* -m|--memory from the command-line *) if !memory_stat then - ppnl - (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes"); + Feedback.msg_notice + (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()); end; begin (* operf-macro interface: @@ -141,7 +143,7 @@ let remove_top_ml () = Mltop.remove () let inputstate = ref "" let set_inputstate s = - let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in + let () = Feedback.msg_warning (str "The inputstate option is deprecated and discouraged.") in inputstate:=s let inputstate () = if not (String.is_empty !inputstate) then @@ -150,7 +152,7 @@ let inputstate () = let outputstate = ref "" let set_outputstate s = - let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in + let () = Feedback.msg_warning (str "The outputstate option is deprecated and discouraged.") in outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then @@ -243,7 +245,7 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; - Pp.make_pp_emacs (); + Feedback.(set_logger emacs_logger); Vernacentries.qed_display_script := false; color := `OFF @@ -646,7 +648,7 @@ let init_toplevel arglist = if !batch_mode then begin flush_all(); if !output_context then - Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); + Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); Profile.print_profile (); exit 0 end diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 367425546..f995a390c 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -150,7 +150,7 @@ let alarm what internal msg = | UserAutomaticRequest | InternalTacticRequest -> (if debug then - msg_warning + Feedback.msg_warning (hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None | _ -> Some msg @@ -303,7 +303,7 @@ let declare_congr_scheme ind = then ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind) else - msg_warning (strbrk "Cannot build congruence scheme because eq is not found") + Feedback.msg_warning (strbrk "Cannot build congruence scheme because eq is not found") end let declare_sym_scheme ind = diff --git a/toplevel/locality.ml b/toplevel/locality.ml index ef789aa5c..c4c891b89 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -35,7 +35,7 @@ let enforce_locality_full locality_flag local = Errors.error "Use only prefix \"Local\"." | None -> if local then begin - Pp.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix."); + Feedback.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix."); Some true end else None diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index d60c73939..52117f13f 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -568,7 +568,7 @@ let is_not_small_constr = function let rec define_keywords_aux = function | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l when is_not_small_constr e -> - Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); + Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l @@ -577,7 +577,7 @@ let rec define_keywords_aux = function (* Ensure that IDENT articulation terminal symbols are keywords *) let define_keywords = function | GramConstrTerminal(IDENT k)::l -> - Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); + Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l @@ -855,12 +855,12 @@ let check_rule_productivity l = let is_not_printable onlyparse noninjective = function | NVar _ -> let () = if not onlyparse then - msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.") + Feedback.msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.") in true | _ -> if not onlyparse && noninjective then - let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in + let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in true else onlyparse @@ -886,7 +886,7 @@ let find_precedence lev etyps symbols = | ETName | ETBigint | ETReference -> begin match lev with | None -> - ([msg_info,strbrk "Setting notation at level 0."],0) + ([Feedback.msg_info,strbrk "Setting notation at level 0."],0) | Some 0 -> ([],0) | _ -> @@ -904,7 +904,7 @@ let find_precedence lev etyps symbols = else [],Option.get lev) | Terminal _ when last_is_terminal () -> if Option.is_empty lev then - ([msg_info,strbrk "Setting notation at level 0."], 0) + ([Feedback.msg_info,strbrk "Setting notation at level 0."], 0) else [],Option.get lev | _ -> if Option.is_empty lev then error "Cannot determine the level."; @@ -931,7 +931,7 @@ let remove_curly_brackets l = (match next' with | Terminal "}" as t2 :: l'' as l1 -> if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then - msg_warning (strbrk "Skipping spaces inside curly brackets"); + Feedback.msg_warning (strbrk "Skipping spaces inside curly brackets"); if deb && List.is_empty l'' then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' @@ -976,7 +976,7 @@ let compute_pure_syntax_data df mods = let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in let msgs = if onlyparse then - (msg_warning, + (Feedback.msg_warning, strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs else msgs in msgs, sy_data, extra diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index d0fa7a80c..36c16208c 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -146,7 +146,7 @@ let dir_ml_load s = let dir_ml_use s = match !load with | WithTop t -> t.use_file s - | _ -> msg_warning (str "Cannot access the ML compiler") + | _ -> Feedback.msg_warning (str "Cannot access the ML compiler") (* Adds a path to the ML paths *) let add_ml_dir s = @@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path = let convert_string d = try Names.Id.of_string d with UserError _ -> - msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); + Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit let add_rec_path ~unix_path ~coq_root ~implicit = @@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let () = List.iter add dirs in Loadpath.add_load_path unix_path ~implicit coq_root else - msg_warning (str "Cannot open " ++ str unix_path) + Feedback.msg_warning (str "Cannot open " ++ str unix_path) (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -324,10 +324,10 @@ let if_verbose_load verb f name ?path fname = let info = str "[Loading ML file " ++ str fname ++ str " ..." in try let path = f name ?path fname in - msg_info (info ++ str " done]"); + Feedback.msg_info (info ++ str " done]"); path with reraise -> - msg_info (info ++ str " failed]"); + Feedback.msg_info (info ++ str " failed]"); raise reraise (** Load a module for the first time (i.e. dynlink it) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 54baa5e3c..dbc3ccaac 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -24,7 +24,7 @@ let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) let trace s = - if !Flags.debug then msg_debug s + if !Flags.debug then Feedback.msg_debug s else () let succfix (depth, fixrels) = @@ -731,11 +731,11 @@ type progress = let obligations_message rem = if rem > 0 then if Int.equal rem 1 then - Flags.if_verbose msg_info (int rem ++ str " obligation remaining") + Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining") else - Flags.if_verbose msg_info (int rem ++ str " obligations remaining") + Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining") else - Flags.if_verbose msg_info (str "No more obligations remaining") + Flags.if_verbose Feedback.msg_info (str "No more obligations remaining") let update_obls prg obls rem = let prg' = { prg with prg_obligations = (obls, rem) } in @@ -992,7 +992,7 @@ and try_solve_obligations n tac = try ignore (solve_obligations n tac) with NoObligations _ -> () and auto_solve_obligations n ?oblset tac : progress = - Flags.if_verbose msg_info (str "Solving obligations automatically..."); + Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically..."); try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent open Pp @@ -1000,13 +1000,13 @@ let show_obligations_of_prg ?(msg=true) prg = let n = prg.prg_name in let obls, rem = prg.prg_obligations in let showed = ref 5 in - if msg then msg_info (int rem ++ str " obligation(s) remaining: "); + if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: "); Array.iteri (fun i x -> match x.obl_body with | None -> if !showed > 0 then ( decr showed; - msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ + Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++ hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++ str "." ++ fnl ()))) @@ -1035,12 +1035,12 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( - Flags.if_verbose msg_info (info ++ str "."); + Flags.if_verbose Feedback.msg_info (info ++ str "."); let cst = declare_definition prg in Defined cst) else ( let len = Array.length obls in - let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in + let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with diff --git a/toplevel/record.ml b/toplevel/record.ml index d12b5ee8e..0c3bd953c 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -196,7 +196,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 msg_warning (hov 0 st) + Flags.if_verbose Feedback.msg_warning (hov 0 st) type field_status = | NoProjection of Name.t @@ -262,7 +262,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field | Some None | None -> false in if not is_primitive then - Flags.if_verbose msg_warning + Flags.if_verbose Feedback.msg_warning (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ str" could not be defined as a primitive record")); is_primitive diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 64225a644..1c3f0d997 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -119,8 +119,7 @@ let verbose_phrase verbch loc = let s = String.create len in seek_in ch (fst loc); really_input ch s 0 len; - ppnl (str s); - pp_flush() + Feedback.msg_notice (str s ++ fnl ()) | None -> () exception End_of_input @@ -152,9 +151,9 @@ let pr_new_syntax loc ocom = | Some com -> Ppvernac.pr_vernac com | None -> mt() in if !beautify_file then - msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) + Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) else - msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); + Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; Format.set_formatter_out_channel stdout @@ -193,14 +192,15 @@ let display_cmd_header loc com = with e -> str (Printexc.to_string e) in let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) in - Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++ - str " [" ++ str cmd ++ str "] "); - Pp.flush_all () + Feedback.msg_notice + (str "Chars " ++ int start ++ str " - " ++ int stop ++ + str " [" ++ str cmd ++ str "] ") + let rec vernac_com verbose checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> - let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in + let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in let st = save_translator_coqdoc () in @@ -248,8 +248,7 @@ and read_vernac_file verbosely s = * raised, which means that we raised the end of the file being loaded *) while true do let loc_ast = parse_sentence input in - vernac_com verbosely checknav loc_ast; - pp_flush () + vernac_com verbosely checknav loc_ast done with any -> (* whatever the exception *) let (e, info) = Errors.push any in @@ -294,7 +293,7 @@ let load_vernac verb file = let ensure_v f = if Filename.check_suffix f ".v" then f else begin - msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \ + Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \ expanded to \"" ++ str f ++ str ".v\""); f ^ ".v" end @@ -304,7 +303,7 @@ let compile verbosely f = let check_pending_proofs () = let pfs = Pfedit.get_all_proof_names () in if not (List.is_empty pfs) then - (msg_error (str "There are pending proofs"); flush_all (); exit 1) in + (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in match !Flags.compilation_mode with | BuildVo -> let long_f_dot_v = ensure_v f in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 23755dac1..222b7d3df 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -57,7 +57,7 @@ let show_proof () = (* spiwack: this would probably be cooler with a bit of polishing. *) let p = Proof_global.give_me_the_proof () in let pprf = Proof.partial_proof p in - msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf) + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf) let show_node () = (* spiwack: I'm have little clue what this function used to do. I deactivated it, @@ -65,22 +65,22 @@ let show_node () = () let show_thesis () = - msg_error (anomaly (Pp.str "TODO") ) + Feedback.msg_error (anomaly (Pp.str "TODO") ) let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = get_pftreestate () in let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in - msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma)) + Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma)) let show_universes () = let pfts = get_pftreestate () in let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in - msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); - msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx) + Feedback.msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); + Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx) let show_prooftree () = (* Spiwack: proof tree is currently not working *) @@ -91,11 +91,10 @@ let enable_goal_printing = ref true let print_subgoals () = if !enable_goal_printing && is_verbose () then begin - msg_notice (pr_open_subgoals ()) + Feedback.msg_notice (pr_open_subgoals ()) end let try_print_subgoals () = - Pp.flush_all(); try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> () @@ -109,10 +108,10 @@ let show_intro all = let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in - msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) + Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) else if not (List.is_empty l) then let n = List.last l in - msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) + Feedback.msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) end (** Prepare a "match" template for a given inductive type. @@ -153,7 +152,7 @@ let show_match id = let pr_branch l = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" in - msg_notice (v 1 (str "match # with" ++ fnl () ++ + Feedback.msg_notice (v 1 (str "match # with" ++ fnl () ++ prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())) (* "Print" commands *) @@ -194,23 +193,23 @@ let print_module r = let globdir = Nametab.locate_dir qid in match globdir with DirModule (dirpath,(mp,_)) -> - msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp) + Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp) | _ -> raise Not_found with - Not_found -> msg_error (str"Unknown Module " ++ pr_qualid qid) + Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid) let print_modtype r = let (loc,qid) = qualid_of_reference r in try let kn = Nametab.locate_modtype qid in - msg_notice (Printmod.print_modtype kn) + Feedback.msg_notice (Printmod.print_modtype kn) with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - msg_notice (Printmod.print_module false mp) + Feedback.msg_notice (Printmod.print_module false mp) with Not_found -> - msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid) + Feedback.msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid) let print_namespace ns = let ns = List.rev (Names.DirPath.repr ns) in @@ -279,7 +278,7 @@ let print_namespace ns = acc ) constants (str"") in - msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace) + Feedback.msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace) let print_strategy r = let open Conv_oracle in @@ -309,7 +308,7 @@ let print_strategy r = else str "Constant strategies" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_strategy cst_lvl) in - msg_notice (var_msg ++ cst_msg) + Feedback.msg_notice (var_msg ++ cst_msg) | Some r -> let r = Smartlocate.smart_global r in let key = match r with @@ -318,7 +317,7 @@ let print_strategy r = | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable" in let lvl = get_strategy oracle key in - msg_notice (pr_strategy (r, lvl)) + Feedback.msg_notice (pr_strategy (r, lvl)) let dump_universes_gen g s = let output = open_out s in @@ -352,7 +351,7 @@ let dump_universes_gen g s = try UGraph.dump_universes output_constraint g; close (); - msg_info (str "Universes written to file \"" ++ str s ++ str "\".") + Feedback.msg_info (str "Universes written to file \"" ++ str s ++ str "\".") with reraise -> let reraise = Errors.push reraise in close (); @@ -367,11 +366,11 @@ let locate_file f = let msg_found_library = function | Library.LibLoaded, fulldir, file -> - msg_info (hov 0 + Feedback.msg_info (hov 0 (pr_dirpath fulldir ++ strbrk " has been loaded from file " ++ str file)) | Library.LibInPath, fulldir, file -> - msg_info (hov 0 + Feedback.msg_info (hov 0 (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file)) let err_unmapped_library loc ?from qid = @@ -506,7 +505,7 @@ let vernac_exact_proof c = called only at the begining of a proof. *) let status = by (Tactics.exact_proof c) in save_proof (Vernacexpr.(Proved(Opaque None,None))); - if not status then Pp.feedback Feedback.AddedAxiom + if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption locality poly (local, kind) l nl = let local = enforce_locality_exp locality local in @@ -518,7 +517,7 @@ let vernac_assumption locality poly (local, kind) l nl = if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl) l; let status = do_assumptions kind nl l in - if not status then Pp.feedback Feedback.AddedAxiom + if not status then Feedback.feedback Feedback.AddedAxiom let vernac_record k poly finite struc binders sort nameopt cfs = let const = match nameopt with @@ -636,7 +635,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef loc mp "mod"; - if_verbose msg_info (str "Module " ++ pr_id id ++ str " is declared"); + if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -657,7 +656,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = export id binders_ast mty_ast_o in Dumpglob.dump_moddef loc mp "mod"; - if_verbose msg_info + if_verbose Feedback.msg_info (str "Interactive Module " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> @@ -675,7 +674,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef loc mp "mod"; - if_verbose msg_info + if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export @@ -683,7 +682,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref loc mp "mod"; - if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined"); + if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = @@ -704,7 +703,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = id binders_ast mty_sign in Dumpglob.dump_moddef loc mp "modtype"; - if_verbose msg_info + if_verbose Feedback.msg_info (str "Interactive Module Type " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> @@ -723,13 +722,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef loc mp "modtype"; - if_verbose msg_info + if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref loc mp "modtype"; - if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined") + if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_include l = Declaremods.declare_include Modintern.interp_module_ast l @@ -797,7 +796,7 @@ let vernac_coercion locality poly local ref qids qidt = let source = cl_of_qualid qids in let ref' = smart_global ref in Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target; - if_verbose msg_info (pr_global ref' ++ str " is now a coercion") + if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion locality poly local id qids qidt = let local = enforce_locality locality local in @@ -813,7 +812,7 @@ let vernac_instance abst locality poly sup inst props pri = ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri) let vernac_context poly l = - if not (Classes.context poly l) then Pp.feedback Feedback.AddedAxiom + if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom let vernac_declare_instances locality ids pri = let glob = not (make_section_locality locality) in @@ -869,7 +868,7 @@ let vernac_set_used_variables e = (* Auxiliary file management *) let expand filename = - Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename + Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename let vernac_add_loadpath implicit pdir ldiropt = let pdir = expand pdir in @@ -889,13 +888,13 @@ let vernac_declare_ml_module locality l = Mltop.declare_ml_modules local (List.map expand l) let vernac_chdir = function - | None -> msg_notice (str (Sys.getcwd())) + | None -> Feedback.msg_notice (str (Sys.getcwd())) | Some path -> begin try Sys.chdir (expand path) - with Sys_error err -> msg_warning (str "Cd failed: " ++ str err) + with Sys_error err -> Feedback.msg_warning (str "Cd failed: " ++ str err) end; - if_verbose msg_info (str (Sys.getcwd())) + if_verbose Feedback.msg_info (str (Sys.getcwd())) (********************) @@ -1068,7 +1067,7 @@ let vernac_declare_arguments locality r l nargs flags = some_scopes_specified || some_simpl_flags_specified) && no_flags then - msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'") + Feedback.msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'") let default_env () = { @@ -1423,7 +1422,7 @@ let vernac_check_may_eval redexp glopt rc = | None -> let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in - msg_notice (print_judgment env sigma' j ++ + Feedback.msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ Printer.pr_universe_ctx sigma uctx) | Some r -> @@ -1434,7 +1433,7 @@ let vernac_check_may_eval redexp glopt rc = let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in c in - msg_notice (print_eval redfun env sigma' rc j) + Feedback.msg_notice (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = let local = make_locality locality in @@ -1450,7 +1449,7 @@ let vernac_global_check c = let senv = Safe_typing.add_constraints cstrs senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - msg_notice (print_safe_judgment env sigma j) + Feedback.msg_notice (print_safe_judgment env sigma j) let get_nth_goal n = @@ -1487,7 +1486,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | NoHyp | Not_found -> print_about ref_or_by_not -let vernac_print = function +let vernac_print = let open Feedback in function | PrintTables -> msg_notice (print_tables ()) | PrintFullContext-> msg_notice (print_full_context_typ ()) | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid) @@ -1586,6 +1585,7 @@ let vernac_search s gopt r = | Some g -> snd (Pfedit.get_goal_context g) , Some g in let get_pattern c = snd (intern_constr_pattern env c) in + let open Feedback in match s with | SearchPattern c -> msg_notice (Search.search_pattern gopt (get_pattern c) r) @@ -1596,8 +1596,8 @@ let vernac_search s gopt r = | SearchAbout sl -> msg_notice (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r) -let vernac_locate = function - | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) +let vernac_locate = let open Feedback in function + | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) | LocateTerm (AN qid) -> msg_notice (print_located_term qid) | LocateAny (ByNotation (_, ntn, sc)) (** TODO : handle Ltac notations *) | LocateTerm (ByNotation (_, ntn, sc)) -> @@ -1640,7 +1640,7 @@ let vernac_unfocus () = let vernac_unfocused () = let p = Proof_global.give_me_the_proof () in if Proof.unfocused p then - msg_notice (str"The proof is indeed fully unfocused.") + Feedback.msg_notice (str"The proof is indeed fully unfocused.") else error "The proof is not fully unfocused." @@ -1668,7 +1668,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) = Proof_global.simple_with_current_proof (fun _ p -> Proof_global.Bullet.put p bullet) -let vernac_show = function +let vernac_show = let open Feedback in function | ShowGoal goalref -> let info = match goalref with | OpenSubgoals -> pr_open_subgoals () @@ -1706,7 +1706,7 @@ let vernac_check_guard () = with UserError(_,s) -> (str ("Condition violated: ") ++s) in - msg_notice message + Feedback.msg_notice message exception End_of_input @@ -1717,7 +1717,7 @@ let vernac_load interp fname = | Some x -> x | None -> raise End_of_input) in let fname = - Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in + Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let input = let longfname = Loadpath.locate_file fname in @@ -1849,15 +1849,15 @@ let interp ?proof ~loc locality poly c = | VernacSearch (s,g,r) -> vernac_search s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r - | VernacComments l -> if_verbose msg_info (str "Comments ok\n") + | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm") - | VernacAbortAll -> msg_warning (str "VernacAbortAll not handled by Stm") - | VernacRestart -> msg_warning (str "VernacRestart not handled by Stm") - | VernacUndo _ -> msg_warning (str "VernacUndo not handled by Stm") - | VernacUndoTo _ -> msg_warning (str "VernacUndoTo not handled by Stm") - | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm") + | VernacAbort id -> Feedback.msg_warning (str "VernacAbort not handled by Stm") + | VernacAbortAll -> Feedback.msg_warning (str "VernacAbortAll not handled by Stm") + | VernacRestart -> Feedback.msg_warning (str "VernacRestart not handled by Stm") + | VernacUndo _ -> Feedback.msg_warning (str "VernacUndo not handled by Stm") + | VernacUndoTo _ -> Feedback.msg_warning (str "VernacUndoTo not handled by Stm") + | VernacBacktrack _ -> Feedback.msg_warning (str "VernacBacktrack not handled by Stm") (* Proof management *) | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false @@ -1991,7 +1991,7 @@ let with_fail b f = | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed!") | HasFailed msg -> - if is_verbose () || !test_mode || !ide_slave then msg_info + if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end @@ -2016,7 +2016,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v | VernacRedirect (s, (_,v)) -> - Pp.with_output_to_file s (aux false) v + Feedback.with_output_to_file s (aux false) v | VernacTime (_,v) -> System.with_time !Flags.time (aux ?locality ?polymorphism isprogcmd) v; diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 7fbd2b119..1116a3104 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -55,7 +55,7 @@ let call ?locality (opn,converted_args) = | Egramml.GramNonTerminal _ -> str "_" in let pr = pr_sequence pr_gram rules in - msg_warning (str "Deprecated vernacular command: " ++ pr) + Feedback.msg_warning (str "Deprecated vernacular command: " ++ pr) in loc:= "Checking arguments"; let hunk = callback converted_args in @@ -68,5 +68,5 @@ let call ?locality (opn,converted_args) = | reraise -> let reraise = Errors.push reraise in if !Flags.debug then - msg_debug (str"Vernac Interpreter " ++ str !loc); + Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc); iraise reraise -- cgit v1.2.3