--- a/src/Pure/Isar/toplevel.ML Sat May 29 15:00:52 2004 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat May 29 15:01:36 2004 +0200
@@ -412,7 +412,7 @@
if int orelse not int_only then ()
else warning (command_msg "Interactive-only " tr);
val (result, opt_exn) =
- (if ! Library.timing andalso not no_timing then (warning (command_msg "" tr); timeap) else I)
+ (if ! Output.timing andalso not no_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 Sat May 29 15:00:52 2004 +0200
+++ b/src/Pure/Thy/thy_info.ML Sat May 29 15:01:36 2004 +0200
@@ -341,7 +341,7 @@
((case new_deps of
Some deps => change_thys (update_node name parents (deps, thy))
| None => ());
- load_thy really ml (time orelse ! Library.timing) initiators dir name parents;
+ load_thy really ml (time orelse ! Output.timing) initiators dir name parents;
false);
in (visited', (result, name)) end
end;
--- a/src/Pure/goals.ML Sat May 29 15:00:52 2004 +0200
+++ b/src/Pure/goals.ML Sat May 29 15:01:36 2004 +0200
@@ -825,7 +825,7 @@
(case Seq.pull (tac st0) of
Some(st,_) => st
| _ => error ("prove_goal: tactic failed"))
- in mkresult (check, cond_timeit (!Library.timing) statef) end
+ in mkresult (check, cond_timeit (!Output.timing) statef) end
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
writeln ("The exception above was raised for\n" ^
Display.string_of_cterm chorn); raise e);
@@ -833,9 +833,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 Library.timing false (prove_goalw_cterm_general true rths chorn)
+ setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
and prove_goalw_cterm_nocheck rths chorn =
- setmp Library.timing false (prove_goalw_cterm_general false rths chorn);
+ setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
(*Version taking the goal as a string*)
@@ -997,7 +997,7 @@
sign_error (Thm.sign_of_thm th, Thm.sign_of_thm th2));
((th2,ths2)::(th,ths)::pairs)));
-fun by tac = cond_timeit (!Library.timing)
+fun by tac = cond_timeit (!Output.timing)
(fn() => make_command (by_com tac));
(* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.