--- a/src/Provers/Arith/abel_cancel.ML Tue May 30 16:02:56 2000 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Tue May 30 16:03:09 2000 +0200
@@ -53,7 +53,7 @@
minus_0, add_0, add_0_right];
(*prove while suppressing timing information*)
- fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
+ fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
val minus = Const ("uminus", Data.T --> Data.T);
--- a/src/Provers/Arith/assoc_fold.ML Tue May 30 16:02:56 2000 +0200
+++ b/src/Provers/Arith/assoc_fold.ML Tue May 30 16:03:09 2000 +0200
@@ -27,7 +27,7 @@
(*prove while suppressing timing information*)
fun prove name ct tacf =
- setmp Goals.proof_timing false (prove_goalw_cterm [] ct) tacf
+ setmp Library.timing false (prove_goalw_cterm [] ct) tacf
handle ERROR =>
error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
@@ -77,7 +77,7 @@
(*test data:
-set proof_timing;
+set timing;
Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)";
--- a/src/Pure/Isar/outer_syntax.ML Tue May 30 16:02:56 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Tue May 30 16:03:09 2000 +0200
@@ -443,7 +443,7 @@
(if time then
timeit (fn () =>
(writeln ("\n**** Starting theory " ^ quote name ^ " ****");
- setmp Goals.proof_timing true (run_thy name) path;
+ setmp Library.timing true (run_thy name) path;
writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
else run_thy name path;
Context.context (ThyInfo.get_theory name);
--- a/src/Pure/Isar/toplevel.ML Tue May 30 16:02:56 2000 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue May 30 16:03:09 2000 +0200
@@ -52,7 +52,6 @@
val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
val quiet: bool ref
- val trace: bool ref
val exn_message: exn -> string
val apply: bool -> transition -> state -> (state * (exn * string) option) option
val excursion: transition list -> unit
@@ -345,7 +344,6 @@
(** toplevel transactions **)
val quiet = ref false;
-val trace = ref false;
(* print exceptions *)
@@ -389,7 +387,7 @@
if int orelse not int_only then ()
else warning (command_msg "Interactive-only " tr);
val (result, opt_exn) =
- (if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
+ (if ! Library.timing then (warning (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
val _ = if int andalso print andalso not (! quiet) then print_state false result else ();
in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
--- a/src/Pure/Thy/thy_info.ML Tue May 30 16:02:56 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue May 30 16:03:09 2000 +0200
@@ -246,7 +246,7 @@
let val name = Path.pack path in
timeit (fn () =>
(writeln ("\n**** Starting file " ^ quote name ^ " ****");
- run_file path;
+ setmp Library.timing true run_file path;
writeln ("**** Finished file " ^ quote name ^ " ****\n")))
end
else run_file path;
@@ -307,10 +307,11 @@
end)
end);
-fun require_thy ml time strict keep_strict initiators prfx (visited, str) =
+fun require_thy ml time_arg strict keep_strict initiators prfx (visited, str) =
let
val path = Path.expand (Path.unpack str);
val name = Path.pack (Path.base path);
+ val time = time_arg orelse ! Library.timing;
in
if name mem_string initiators then error (cycle_msg name initiators) else ();
if known_thy name andalso is_finished name orelse name mem_string visited then
--- a/src/Pure/goals.ML Tue May 30 16:02:56 2000 +0200
+++ b/src/Pure/goals.ML Tue May 30 16:03:09 2000 +0200
@@ -63,7 +63,6 @@
val pprint_typ : typ -> pprint_args -> unit
val print_exn : exn -> 'a
val print_sign_exn : Sign.sg -> exn -> 'a
- val proof_timing : bool ref
val prove_goal : theory -> string -> (thm list -> tactic list) -> thm
val prove_goalw : theory->thm list->string->(thm list->tactic list)->thm
val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
@@ -93,9 +92,6 @@
(*** References ***)
-(*Should process time be printed after proof steps?*)
-val proof_timing = ref false;
-
(*Current assumption list -- set by "goal".*)
val curr_prems = ref([] : thm list);
@@ -276,7 +272,7 @@
(case Seq.pull (tac st0) of
Some(st,_) => st
| _ => error ("prove_goal: tactic failed"))
- in mkresult (check, cond_timeit (!proof_timing) statef) end
+ in mkresult (check, cond_timeit (!Library.timing) statef) end
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
writeln ("The exception above was raised for\n" ^
string_of_cterm chorn); raise e);
@@ -284,9 +280,9 @@
(*Two variants: one checking the result, one not.
Neither prints runtime messages: they are for internal packages.*)
fun prove_goalw_cterm rths chorn =
- setmp proof_timing false (prove_goalw_cterm_general true rths chorn)
+ setmp Library.timing false (prove_goalw_cterm_general true rths chorn)
and prove_goalw_cterm_nocheck rths chorn =
- setmp proof_timing false (prove_goalw_cterm_general false rths chorn);
+ setmp Library.timing false (prove_goalw_cterm_general false rths chorn);
(*Version taking the goal as a string*)
@@ -448,7 +444,7 @@
sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
((th2,ths2)::(th,ths)::pairs)));
-fun by tac = cond_timeit (!proof_timing)
+fun by tac = cond_timeit (!Library.timing)
(fn() => make_command (by_com tac));
(* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.
--- a/src/Pure/library.ML Tue May 30 16:02:56 2000 +0200
+++ b/src/Pure/library.ML Tue May 30 16:03:09 2000 +0200
@@ -244,6 +244,7 @@
val cond_timeit: bool -> (unit -> 'a) -> 'a
val timeit: (unit -> 'a) -> 'a
val timeap: ('a -> 'b) -> 'a -> 'b
+ val timing: bool ref
(*misc*)
val make_keylist: ('a -> 'b) -> 'a list -> ('a * 'b) list
@@ -1178,14 +1179,12 @@
(** timing **)
(*a conditional timing function: applies f to () and, if the flag is true,
- prints its runtime*)
+ prints its runtime on warning channel*)
fun cond_timeit flag f =
if flag then
let val start = startTiming()
val result = f ()
- in
- writeln (endTiming start); result
- end
+ in warning (endTiming start); result end
else f ();
(*unconditional timing function*)
@@ -1194,6 +1193,9 @@
(*timed application function*)
fun timeap f x = timeit (fn () => f x);
+(*global timing mode*)
+val timing = ref false;
+
(** misc **)