diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 18:03:06 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 18:03:06 +0000 |
| commit | cf7660a3a8932ee593a376e8ec7ec251896a72e3 (patch) | |
| tree | 5f3fd167f5dd704bf5482d236624aa8ef8bf6707 /toplevel/vernac.ml | |
| parent | 35e4ac349af4fabbc5658b5cba632f98ec04da3f (diff) | |
Getting rid of Pp.msgnl and Pp.message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 6d37e0d78..d6178cd62 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -159,9 +159,9 @@ let verbose_phrase verbch loc = let s = String.create len in seek_in ch (fst loc); really_input ch s 0 len; - message s; + ppnl (str s); pp_flush() - | _ -> () + | None -> () exception End_of_input @@ -194,7 +194,7 @@ let pr_new_syntax loc ocom = if !beautify_file then pp (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) else - msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); + msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; Format.set_formatter_out_channel stdout @@ -251,7 +251,7 @@ let rec vernac_com interpfun checknav (loc,com) = | e -> (* Anomalies are re-raised by the next line *) let msg = Errors.print_no_anomaly e in - if_verbose msgnl + if_verbose msg_info (str "The command has indeed failed with message:" ++ fnl () ++ str "=> " ++ hov 0 msg) end @@ -260,7 +260,7 @@ let rec vernac_com interpfun checknav (loc,com) = let tstart = System.get_time() in interp v; let tend = get_time() in - msgnl (str"Finished transaction in " ++ + msg_info (str"Finished transaction in " ++ System.fmt_time_difference tstart tend) | VernacTimeout(n,v) -> @@ -357,7 +357,7 @@ let compile verbosely f = if !Flags.xml_export then !xml_start_library (); let _ = load_vernac verbosely long_f_dot_v in if Pfedit.get_all_proof_names () <> [] then - (message "Error: There are pending proofs"; exit 1); + (pperrnl (str "Error: There are pending proofs"); exit 1); if !Flags.xml_export then !xml_end_library (); Dumpglob.end_dump_glob (); Library.save_library_to ldir (long_f_dot_v ^ "o") |