1.1 --- a/src/Provers/Arith/abel_cancel.ML	Tue May 30 16:02:56 2000 +0200
     1.2 +++ b/src/Provers/Arith/abel_cancel.ML	Tue May 30 16:03:09 2000 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  				    minus_0, add_0, add_0_right];
     1.5  
     1.6   (*prove while suppressing timing information*)
     1.7 - fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
     1.8 + fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
     1.9  
    1.10   val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
    1.11   val minus = Const ("uminus", Data.T --> Data.T);

     2.1 --- a/src/Provers/Arith/assoc_fold.ML	Tue May 30 16:02:56 2000 +0200
     2.2 +++ b/src/Provers/Arith/assoc_fold.ML	Tue May 30 16:03:09 2000 +0200
     2.3 @@ -27,7 +27,7 @@
     2.4  
     2.5   (*prove while suppressing timing information*)
     2.6   fun prove name ct tacf = 
     2.7 -     setmp Goals.proof_timing false (prove_goalw_cterm [] ct) tacf
     2.8 +     setmp Library.timing false (prove_goalw_cterm [] ct) tacf
     2.9       handle ERROR =>
    2.10  	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
    2.11                  
    2.12 @@ -77,7 +77,7 @@
    2.13  
    2.14  
    2.15  (*test data:
    2.16 -set proof_timing;
    2.17 +set timing;
    2.18  
    2.19  Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)";
    2.20  

     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue May 30 16:02:56 2000 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue May 30 16:03:09 2000 +0200
     3.3 @@ -443,7 +443,7 @@
     3.4   (if time then
     3.5      timeit (fn () =>
     3.6       (writeln ("\n**** Starting theory " ^ quote name ^ " ****");
     3.7 -      setmp Goals.proof_timing true (run_thy name) path;
     3.8 +      setmp Library.timing true (run_thy name) path;
     3.9        writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
    3.10    else run_thy name path;
    3.11    Context.context (ThyInfo.get_theory name);

     4.1 --- a/src/Pure/Isar/toplevel.ML	Tue May 30 16:02:56 2000 +0200
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Tue May 30 16:03:09 2000 +0200
     4.3 @@ -52,7 +52,6 @@
     4.4    val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
     4.5    val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
     4.6    val quiet: bool ref
     4.7 -  val trace: bool ref
     4.8    val exn_message: exn -> string
     4.9    val apply: bool -> transition -> state -> (state * (exn * string) option) option
    4.10    val excursion: transition list -> unit
    4.11 @@ -345,7 +344,6 @@
    4.12  (** toplevel transactions **)
    4.13  
    4.14  val quiet = ref false;
    4.15 -val trace = ref false;
    4.16  
    4.17  
    4.18  (* print exceptions *)
    4.19 @@ -389,7 +387,7 @@
    4.20        if int orelse not int_only then ()
    4.21        else warning (command_msg "Interactive-only " tr);
    4.22      val (result, opt_exn) =
    4.23 -      (if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
    4.24 +      (if ! Library.timing then (warning (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
    4.25      val _ = if int andalso print andalso not (! quiet) then print_state false result else ();
    4.26    in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
    4.27  

     5.1 --- a/src/Pure/Thy/thy_info.ML	Tue May 30 16:02:56 2000 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Tue May 30 16:03:09 2000 +0200
     5.3 @@ -246,7 +246,7 @@
     5.4      let val name = Path.pack path in
     5.5        timeit (fn () =>
     5.6         (writeln ("\n**** Starting file " ^ quote name ^ " ****");
     5.7 -        run_file path;
     5.8 +        setmp Library.timing true run_file path;
     5.9          writeln ("**** Finished file " ^ quote name ^ " ****\n")))
    5.10      end
    5.11    else run_file path;
    5.12 @@ -307,10 +307,11 @@
    5.13                end)
    5.14        end);
    5.15  
    5.16 -fun require_thy ml time strict keep_strict initiators prfx (visited, str) =
    5.17 +fun require_thy ml time_arg strict keep_strict initiators prfx (visited, str) =
    5.18    let
    5.19      val path = Path.expand (Path.unpack str);
    5.20      val name = Path.pack (Path.base path);
    5.21 +    val time = time_arg orelse ! Library.timing;
    5.22    in
    5.23      if name mem_string initiators then error (cycle_msg name initiators) else ();
    5.24      if known_thy name andalso is_finished name orelse name mem_string visited then

     6.1 --- a/src/Pure/goals.ML	Tue May 30 16:02:56 2000 +0200
     6.2 +++ b/src/Pure/goals.ML	Tue May 30 16:03:09 2000 +0200
     6.3 @@ -63,7 +63,6 @@
     6.4    val pprint_typ	: typ -> pprint_args -> unit
     6.5    val print_exn		: exn -> 'a
     6.6    val print_sign_exn	: Sign.sg -> exn -> 'a
     6.7 -  val proof_timing	: bool ref
     6.8    val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
     6.9    val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
    6.10    val prove_goalw_cterm	: thm list->cterm->(thm list->tactic list)->thm
    6.11 @@ -93,9 +92,6 @@
    6.12  
    6.13  (*** References ***)
    6.14  
    6.15 -(*Should process time be printed after proof steps?*)
    6.16 -val proof_timing = ref false;
    6.17 -
    6.18  (*Current assumption list -- set by "goal".*)
    6.19  val curr_prems = ref([] : thm list);
    6.20  
    6.21 @@ -276,7 +272,7 @@
    6.22  	  (case Seq.pull (tac st0) of 
    6.23  	       Some(st,_) => st
    6.24  	     | _ => error ("prove_goal: tactic failed"))
    6.25 -  in  mkresult (check, cond_timeit (!proof_timing) statef)  end
    6.26 +  in  mkresult (check, cond_timeit (!Library.timing) statef)  end
    6.27    handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
    6.28  	       writeln ("The exception above was raised for\n" ^ 
    6.29  		      string_of_cterm chorn); raise e);
    6.30 @@ -284,9 +280,9 @@
    6.31  (*Two variants: one checking the result, one not.  
    6.32    Neither prints runtime messages: they are for internal packages.*)
    6.33  fun prove_goalw_cterm rths chorn = 
    6.34 -	setmp proof_timing false (prove_goalw_cterm_general true rths chorn)
    6.35 +	setmp Library.timing false (prove_goalw_cterm_general true rths chorn)
    6.36  and prove_goalw_cterm_nocheck rths chorn = 
    6.37 -	setmp proof_timing false (prove_goalw_cterm_general false rths chorn);
    6.38 +	setmp Library.timing false (prove_goalw_cterm_general false rths chorn);
    6.39  
    6.40  
    6.41  (*Version taking the goal as a string*)
    6.42 @@ -448,7 +444,7 @@
    6.43  		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
    6.44         ((th2,ths2)::(th,ths)::pairs)));
    6.45  
    6.46 -fun by tac = cond_timeit (!proof_timing) 
    6.47 +fun by tac = cond_timeit (!Library.timing) 
    6.48      (fn() => make_command (by_com tac));
    6.49  
    6.50  (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.

     7.1 --- a/src/Pure/library.ML	Tue May 30 16:02:56 2000 +0200
     7.2 +++ b/src/Pure/library.ML	Tue May 30 16:03:09 2000 +0200
     7.3 @@ -244,6 +244,7 @@
     7.4    val cond_timeit: bool -> (unit -> 'a) -> 'a
     7.5    val timeit: (unit -> 'a) -> 'a
     7.6    val timeap: ('a -> 'b) -> 'a -> 'b
     7.7 +  val timing: bool ref
     7.8  
     7.9    (*misc*)
    7.10    val make_keylist: ('a -> 'b) -> 'a list -> ('a * 'b) list
    7.11 @@ -1178,14 +1179,12 @@
    7.12  (** timing **)
    7.13  
    7.14  (*a conditional timing function: applies f to () and, if the flag is true,
    7.15 -  prints its runtime*)
    7.16 +  prints its runtime on warning channel*)
    7.17  fun cond_timeit flag f =
    7.18    if flag then
    7.19      let val start = startTiming()
    7.20          val result = f ()
    7.21 -    in
    7.22 -        writeln (endTiming start);  result
    7.23 -    end
    7.24 +    in warning (endTiming start);  result end
    7.25    else f ();
    7.26  
    7.27  (*unconditional timing function*)
    7.28 @@ -1194,6 +1193,9 @@
    7.29  (*timed application function*)
    7.30  fun timeap f x = timeit (fn () => f x);
    7.31  
    7.32 +(*global timing mode*)
    7.33 +val timing = ref false;
    7.34 +
    7.35  
    7.36  
    7.37  (** misc **)