Merge PR #9316: Fix #3934: coqc -time -quick gives unreadable output

3 files changed, 25 insertions, 2 deletions

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 4065bb9c1f..b4b893a3fd 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -406,3 +406,24 @@ let with_output_to_file fname func input =
     deep_ft := Util.pi3 old_fmt;
     close_out channel;
     Exninfo.iraise reraise
+
+(* For coqtop -time, we display the position in the file,
+   and a glimpse of the executed command *)
+
+let pr_cmd_header {CAst.loc;v=com} =
+  let shorten s =
+    if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
+  in
+  let noblank s = String.map (fun c ->
+      match c with
+        | ' ' | '\n' | '\t' | '\r' -> '~'
+        | x -> x
+      ) s
+  in
+  let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+  let safe_pr_vernac x =
+    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 str "Chars " ++ int start ++ str " - " ++ int stop ++
+     str " [" ++ str cmd ++ str "] "
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 0ddf474970..5f84c5edee 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -71,3 +71,4 @@ val print_err_exn : exn -> unit
     redirected to a file [file] *)
 val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
 
+val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e6e3db4beb..dbccea1117 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2388,8 +2388,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
     control v
   | VernacRedirect (s, {v}) ->
     Topfmt.with_output_to_file s control v
-  | VernacTime (batch, {v}) ->
-    System.with_time ~batch control v;
+  | VernacTime (batch, com) ->
+    let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in
+    System.with_time ~batch ~header control com.CAst.v;
 
   and aux ~atts : _ -> unit =
     function