coqtop -time : display per-command timings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15859 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 35 insertions, 6 deletions

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 9b2054400..efff8dbc6 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -139,7 +139,7 @@ let parse_args () =
     | "-R" :: s :: "-as" :: [] -> usage ()
     | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
 
-    | ("-notactics"|"-debug"|"-nolib"|"-boot"
+    | ("-notactics"|"-debug"|"-nolib"|"-boot"|"-time"
       |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index fe612f710..64e98d641 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -246,6 +246,8 @@ let parse_args arglist =
 
     | "-debug" :: rem -> set_debug (); parse rem
 
+    | "-time" :: rem -> Vernac.time := true; parse rem
+
     | "-compat" :: v :: rem ->
         Flags.compat_version := get_compat_version v; parse rem
     | "-compat" :: []       -> usage ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 4751f7e32..8e1864461 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -72,6 +72,7 @@ let print_usage_channel co command =
 \n                         stdout (if unset)\
 \n  -quality               improve the legibility of the proof terms produced by\
 \n                         some tactics\
+\n  -time                  display the time taken by each command\
 \n  -h, --help             print this list of options\
 \n"
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b897a6d91..7cff9a4ec 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -15,7 +15,6 @@ open Flags
 open System
 open Vernacexpr
 open Vernacinterp
-open Ppvernac
 
 (* The functions in this module may raise (unexplainable!) exceptions.
    Use the module Coqtoplevel, which catches these exceptions
@@ -47,6 +46,28 @@ let is_reset = function
   | VernacResetInitial | VernacResetName _ -> true
   | _ -> false
 
+(* For coqtop -time, we display the position in the file,
+   and a glimpse of the executed command *)
+
+let time = ref false
+
+let display_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
+      match s.[i] with
+	| ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~'
+	| _ -> ()
+    done;
+    s
+  in
+  let (start,stop) = Loc.unloc loc in
+  let cmd = noblank (shorten (string_of_ppcmds (Ppvernac.pr_vernac com)))
+  in
+  Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
+	 str (" ["^cmd^"] "));
+  Pp.flush_all ()
+
 (* When doing Load on a file, two behaviors are possible:
 
    - either the history stack is grown by only one command,
@@ -217,7 +238,7 @@ let pr_new_syntax loc ocom =
   let fs = States.freeze () in
   let com = match ocom with
     | Some VernacNop -> mt()
-    | Some com -> pr_vernac com
+    | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
   if !beautify_file then
     pp (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
@@ -290,9 +311,9 @@ let rec vernac_com interpfun checknav (loc,com) =
     | VernacTime v ->
 	  let tstart = System.get_time() in
           let status = interp v in
-	  let tend = get_time() in
-          msg_info (str"Finished transaction in " ++
-                   System.fmt_time_difference tstart tend);
+	  let tend = System.get_time() in
+	  let msg = if !time then "" else "Finished transaction in " in
+          msg_info (str msg ++ System.fmt_time_difference tstart tend);
           status
 
     | VernacTimeout(n,v) ->
@@ -314,6 +335,8 @@ let rec vernac_com interpfun checknav (loc,com) =
       checknav loc com;
       current_timeout := !default_timeout;
       if do_beautify () then pr_new_syntax loc (Some com);
+      if !time then display_cmd_header loc com;
+      let com = if !time then VernacTime com else com in
       interp com
     with e ->
       Format.set_formatter_out_channel stdout;
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 3c09139ba..8f1fbc54f 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -48,3 +48,6 @@ val compile : bool -> string -> unit
 
 
 val is_navigation_vernac : Vernacexpr.vernac_expr -> bool
+
+(** Should we display timings for each command ? *)
+val time : bool ref