[pp] Fix bug 4842 (Time prints in multiple lines)

This commit proposes a fix for
https://coq.inria.fr/bugs/show_bug.cgi?id=4842

The previous feature is a bit complicated to do correctly due to the
separation over who has control of the console.

Indeed, `-timed` is a command line option of the batch compiler, so we
resort to a hack and assume control over the console. I am not very
happy with this solution but should do the job.

Note that the timing event is still being sent by the standard msg
mechanism. A particular point of interest is the duplication of paths
between the stm and vernac.

1 files changed, 11 insertions, 6 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f83ada466b..b4926cf786 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -158,7 +158,7 @@ let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
 
-let display_cmd_header loc com =
+let pp_cmd_header loc com =
   let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
   let noblank s =
     for i = 0 to String.length s - 1 do
@@ -173,11 +173,15 @@ let display_cmd_header loc com =
     try Ppvernac.pr_vernac x
     with e -> str (Printexc.to_string e) in
   let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
-  in
-  Feedback.msg_notice
-    (str "Chars " ++ int start ++ str " - " ++ int stop ++
-     str " [" ++ str cmd ++ str "] ")
+  in str "Chars " ++ int start ++ str " - " ++ int stop ++
+     str " [" ++ str cmd ++ str "] "
 
+(* This is a special case where we assume we are in console batch mode
+   and take control of the console.
+ *)
+let print_cmd_header loc com =
+  Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
+  Format.pp_print_flush !Pp_control.std_ft ()
 
 let rec vernac_com checknav (loc,com) =
   let interp = function
@@ -208,7 +212,8 @@ let rec vernac_com checknav (loc,com) =
     try
       checknav loc com;
       if do_beautify () then pr_new_syntax loc (Some com);
-      if !Flags.time then display_cmd_header loc com;
+      (* XXX: This is not 100% correct if called from an IDE context *)
+      if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
       let a = CLexer.com_state () in
       interp com;