Merge remote-tracking branch 'github/pr/257' into v8.6

Was PR#257: [checker] Fix/fine tune printing.

4 files changed, 15 insertions, 10 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 863cf7b2c..8b299bf2a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -11,6 +11,8 @@ open CErrors
 open Util
 open Names
 
+let chk_pp = Pp.pp_with Format.std_formatter
+
 let pr_dirpath dp = str (DirPath.to_string dp)
 let default_root_prefix = DirPath.empty
 let split_dirpath d =
@@ -118,7 +120,6 @@ let check_one_lib admit (dir,m) =
     (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 Feedback.msg_notice (fnl());
   register_loaded_library m
 
 (*************************************************************************)
@@ -298,7 +299,7 @@ let name_clash_message dir mdir f =
 let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
-  Flags.if_verbose Feedback.msg_notice(str"[intern "++str f++str" ...");
+  Flags.if_verbose chk_pp (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
@@ -322,7 +323,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
-       Feedback.msg_notice(str " (was a vio file) ");
+       chk_pp (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"))
@@ -333,12 +334,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 Feedback.msg_notice (str" done]");
+      Flags.if_verbose chk_pp (str" done]" ++ fnl ());
       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 Feedback.msg_notice (str" failed!]"); raise e in
+    with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); 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,_,_) ->
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index f196746a5..741f53284 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -57,8 +57,7 @@ let print_context env =
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_ax csts) ++
-       fnl()));
+      str "* " ++ hov 0 (pr_ax csts)));
   end
 
 let stats () =
diff --git a/checker/checker.ml b/checker/checker.ml
index 503697b59..8dbb7e011 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -16,6 +16,8 @@ open Check
 
 let () = at_exit flush_all
 
+let chk_pp = Pp.pp_with Format.std_formatter
+
 let fatal_error info anomaly =
   flush_all (); Feedback.msg_error info; flush_all ();
   exit (if anomaly then 129 else 1)
@@ -283,7 +285,8 @@ let rec explain_exn = function
           Format.printf "@\nis not convertible with@\n";
           Print.print_pure_constr a;
           Format.printf "@\n====== universes ====@\n";
-          Feedback.msg_notice (Univ.pr_universes
+          chk_pp
+            (Univ.pr_universes
             (ctx.Environ.env_stratification.Environ.env_universes));
           str "\nCantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
diff --git a/checker/print.ml b/checker/print.ml
index c0d1ac368..7ef752b00 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -10,7 +10,9 @@ open Format
 open Cic
 open Names
 
-let print_instance i = Feedback.msg_notice (Univ.Instance.pr i)
+let chk_pp = Pp.pp_with Format.std_formatter
+
+let print_instance i = chk_pp (Univ.Instance.pr i)
 
 let print_pure_constr csr =
   let rec term_display c = match  c with
@@ -108,7 +110,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("; Feedback.msg_notice (Univ.pr_uni u); print_string ")"
+    | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")"
 
   and name_display = function
     | Name id -> print_string (Id.to_string id)