# HG changeset patch
# User wenzelm
# Date 1085835696 -7200
# Node ID 8cdf5a813cecdfdb743ce3bdf5c3f3106973f3b6
# Parent  336ade035a34ae8aa15f0839986f6b66079eb4bf
Output.timing;

diff -r 336ade035a34 -r 8cdf5a813cec src/Pure/Isar/toplevel.ML
--- 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;
diff -r 336ade035a34 -r 8cdf5a813cec src/Pure/Thy/thy_info.ML
--- 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;
diff -r 336ade035a34 -r 8cdf5a813cec src/Pure/goals.ML
--- 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.