[checker] Fix/fine tune printing.

In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct
access to the console, recommending instead to provide information to
the user by means of the `Feedback.msg_*` facilities.

However, we introduced a display bug in the checker printer as it is
special and doesn't use the Pp facilities (likely for trust reasons),
spotted by @herbelin

This patch fixes this bug and performs a couple more of fine tunings in
the input.

However, it could be desirable to port the `checker/printer.ml` to `Pp`
and use the feedback mechanism; this would allow IDEs to use the checker
in a more convenient way, at the cost of trusting `Pp` (which is already
a bit trusted currently)

A start of that idea can be found at:
https://github.com/ejgallego/coq/tree/fix_checker_printing

1 files changed, 6 insertions, 5 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,_,_) ->