Output.timing;
authorwenzelm
Sat May 29 15:01:36 2004 +0200 (2004-05-29)
changeset 148258cdf5a813cec
parent 14824 336ade035a34
child 14826 48cfe0fe53e2
Output.timing;
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_info.ML
src/Pure/goals.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat May 29 15:00:52 2004 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat May 29 15:01:36 2004 +0200
     1.3 @@ -412,7 +412,7 @@
     1.4        if int orelse not int_only then ()
     1.5        else warning (command_msg "Interactive-only " tr);
     1.6      val (result, opt_exn) =
     1.7 -      (if ! Library.timing andalso not no_timing then (warning (command_msg "" tr); timeap) else I)
     1.8 +      (if ! Output.timing andalso not no_timing then (warning (command_msg "" tr); timeap) else I)
     1.9          (apply_trans int trans) state;
    1.10      val _ = if int andalso print andalso not (! quiet) then print_state false result else ();
    1.11    in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
     2.1 --- a/src/Pure/Thy/thy_info.ML	Sat May 29 15:00:52 2004 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Sat May 29 15:01:36 2004 +0200
     2.3 @@ -341,7 +341,7 @@
     2.4              ((case new_deps of
     2.5                Some deps => change_thys (update_node name parents (deps, thy))
     2.6              | None => ());
     2.7 -             load_thy really ml (time orelse ! Library.timing) initiators dir name parents;
     2.8 +             load_thy really ml (time orelse ! Output.timing) initiators dir name parents;
     2.9               false);
    2.10        in (visited', (result, name)) end
    2.11    end;
     3.1 --- a/src/Pure/goals.ML	Sat May 29 15:00:52 2004 +0200
     3.2 +++ b/src/Pure/goals.ML	Sat May 29 15:01:36 2004 +0200
     3.3 @@ -825,7 +825,7 @@
     3.4  	  (case Seq.pull (tac st0) of 
     3.5  	       Some(st,_) => st
     3.6  	     | _ => error ("prove_goal: tactic failed"))
     3.7 -  in  mkresult (check, cond_timeit (!Library.timing) statef)  end
     3.8 +  in  mkresult (check, cond_timeit (!Output.timing) statef)  end
     3.9    handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
    3.10  	       writeln ("The exception above was raised for\n" ^ 
    3.11  		      Display.string_of_cterm chorn); raise e);
    3.12 @@ -833,9 +833,9 @@
    3.13  (*Two variants: one checking the result, one not.  
    3.14    Neither prints runtime messages: they are for internal packages.*)
    3.15  fun prove_goalw_cterm rths chorn = 
    3.16 -	setmp Library.timing false (prove_goalw_cterm_general true rths chorn)
    3.17 +	setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
    3.18  and prove_goalw_cterm_nocheck rths chorn = 
    3.19 -	setmp Library.timing false (prove_goalw_cterm_general false rths chorn);
    3.20 +	setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
    3.21  
    3.22  
    3.23  (*Version taking the goal as a string*)
    3.24 @@ -997,7 +997,7 @@
    3.25  		       sign_error (Thm.sign_of_thm th, Thm.sign_of_thm th2));
    3.26         ((th2,ths2)::(th,ths)::pairs)));
    3.27  
    3.28 -fun by tac = cond_timeit (!Library.timing) 
    3.29 +fun by tac = cond_timeit (!Output.timing) 
    3.30      (fn() => make_command (by_com tac));
    3.31  
    3.32  (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.