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

7 files changed, 18 insertions, 19 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 5b8507304b..976120ffec 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -99,11 +99,11 @@ 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 msgnl
+    (Flags.if_verbose ppnl
       (str "Admitting library: " ++ pr_dirpath dir);
       Safe_typing.unsafe_import file md dig)
   else
-    (Flags.if_verbose msgnl
+    (Flags.if_verbose ppnl
       (str "Checking library: " ++ pr_dirpath dir);
       Safe_typing.import file md dig);
   Flags.if_verbose pp (fnl());
@@ -159,7 +159,7 @@ let remove_load_path dir =
 
 let add_load_path (phys_path,coq_path) =
   if !Flags.debug then
-    msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+    ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = canonical_path_name phys_path in
     match list_filter2 (fun p d -> p = phys_path) !load_paths with
@@ -299,9 +299,9 @@ let intern_from_file (dir, f) =
       if dir <> md.md_name then
         errorlabstrm "load_physical_library"
           (name_clash_message dir md.md_name f);
-      Flags.if_verbose msgnl(str" done]");
+      Flags.if_verbose ppnl (str" done]");
       md,table,digest
-    with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
+    with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
   mk_library md f table digest
 
@@ -360,11 +360,11 @@ let recheck_library ~norec ~admit ~check =
   let nochk =
     List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
   (* *)
-  Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
+  Flags.if_verbose ppnl (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 msgnl(str"Modules were successfully checked")
+  Flags.if_verbose ppnl (str"Modules were successfully checked")
 
 open Printf
 
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index cdb0ade744..1cc47fde32 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -55,12 +55,12 @@ let print_context env =
          env_modules=mods; env_modtypes=mtys};
        env_stratification=
         {env_universes=univ; env_engagement=engt}} = env in
-    msgnl(hov 0
+    ppnl(hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
-      fnl()))
+      fnl())); pp_flush()
   end
 
 let stats () =
diff --git a/checker/checker.ml b/checker/checker.ml
index 7ea55d833c..848fd22f4e 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -292,7 +292,7 @@ let parse_args argv =
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
-	(msgnl (str ("Directory '"^s^"' does not exist")); exit 1);
+	(pperrnl (str ("Directory '"^s^"' does not exist")); exit 1);
       Flags.coqlib := s;
       Flags.coqlib_spec := true;
       parse rem
@@ -332,7 +332,7 @@ let parse_args argv =
         Flags.make_silent true; parse rem
 
     | s :: _ when s<>"" && s.[0]='-' ->
-        msgnl (str "Unknown option " ++ str s); exit 1
+        pperrnl (str "Unknown option " ++ str s); exit 1
     | s :: rem ->  add_compile s; parse rem
   in
   try
@@ -342,9 +342,9 @@ let parse_args argv =
 	try
 	  Stream.empty s; exit 1
 	with Stream.Failure ->
-	  msgnl (explain_exn e); exit 1
+	  pperrnl (explain_exn e); exit 1
       end
-    | e -> begin msgnl (explain_exn e); exit 1 end
+    | e -> begin pperrnl (explain_exn e); exit 1 end
 
 
 (* To prevent from doing the initialization twice *)
@@ -361,8 +361,7 @@ let init_with_argv argv =
       engage ();
     with e ->
       flush_all();
-      message "Error during initialization :";
-      msgnl (explain_exn e);
+      pperrnl (str "Error during initialization :" ++ (explain_exn e));
       exit 1
   end
 
diff --git a/checker/closure.ml b/checker/closure.ml
index 069b820176..c30b305575 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() =
-  msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+  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 c12c54cfd9..a8f151e7e2 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -526,7 +526,7 @@ let check_positivity env_ar mind params nrecp inds =
 (************************************************************************)
 
 let check_inductive env kn mib =
-  Flags.if_verbose msgnl (str "  checking ind: " ++ pr_mind kn);
+  Flags.if_verbose ppnl (str "  checking ind: " ++ pr_mind kn); pp_flush ();
   (* check mind_constraints: should be consistent with env *)
   let env = add_constraints mib.mind_constraints env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7a66ced77b..a51b66ce0e 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,7 +26,7 @@ let refresh_arity ar =
     | _ -> ar, Univ.empty_constraint
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose msgnl (str "  checking cst: " ++ prcon kn);
+  Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn);
 (*  let env = add_constraints cb.const_constraints env in*)
   let env' = check_named_ctxt env cb.const_hyps in
   (match cb.const_type with
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 57a9011cfd..7fe37e29d5 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -182,7 +182,7 @@ let stamp_library file digest = ()
    warning is issued in case of mismatch *)
 let import file (dp,mb,depends,engmt as vo) digest =
   Validate.apply !Flags.debug val_vo vo;
-  Flags.if_verbose msgnl (str "*** vo structure validated ***");
+  Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush ();
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;