diff options
| -rw-r--r-- | scripts/coqc.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 33 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 3 |
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 |