src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -42,7 +42,6 @@
   val interactive: bool -> transition -> transition
   val set_print: bool -> transition -> transition
   val print: transition -> transition
-  val no_timing: transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
@@ -346,18 +345,17 @@
   pos: Position.T,           (*source position*)
   int_only: bool,            (*interactive-only*)
   print: bool,               (*print result state*)
-  no_timing: bool,           (*suppress timing*)
   timing: Time.time option,  (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
-fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
+fun make_transition (name, pos, int_only, print, timing, trans) =
   Transition {name = name, pos = pos, int_only = int_only, print = print,
-    no_timing = no_timing, timing = timing, trans = trans};
+    timing = timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
-  make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
+fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) =
+  make_transition (f (name, pos, int_only, print, timing, trans));
 
-val empty = make_transition ("", Position.none, false, false, false, NONE, []);
+val empty = make_transition ("", Position.none, false, false, NONE, []);
 
 
 (* diagnostics *)
@@ -375,26 +373,23 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, int_only, print, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
-fun position pos = map_transition (fn (name, _, int_only, print, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
-fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
-val no_timing = map_transition (fn (name, pos, int_only, print, _, timing, trans) =>
-  (name, pos, int_only, print, true, timing, trans));
-
-fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, tr :: trans));
+fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) =>
+  (name, pos, int_only, print, timing, tr :: trans));
 
-val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, timing, _) =>
-  (name, pos, int_only, print, no_timing, timing, []));
+val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) =>
+  (name, pos, int_only, print, timing, []));
 
-fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
 val print = set_print true;
 
@@ -633,28 +628,26 @@
 (* apply transitions *)
 
 fun get_timing (Transition {timing, ...}) = timing;
-fun put_timing timing = map_transition (fn (name, pos, int_only, print, no_timing, _, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
 local
 
-fun app int (tr as Transition {trans, print, no_timing, ...}) =
+fun app int (tr as Transition {trans, print, ...}) =
   setmp_thread_position tr (fn state =>
     let
       val timing_start = Timing.start ();
 
       val (result, opt_err) =
-         state |>
-          (apply_trans int trans
-            |> (! profiling > 0 andalso not no_timing) ? profile (! profiling));
+         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
       val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
 
       val timing_result = Timing.result timing_start;
 
       val _ =
-        if Timing.is_relevant timing_result andalso
-          (! profiling > 0 orelse ! timing andalso not no_timing)
-        then warning (command_msg "" tr ^ ": " ^ Timing.message timing_result)
+        if Timing.is_relevant timing_result andalso (! profiling > 0 orelse ! timing)
+          andalso not (Keyword.is_control (name_of tr))
+        then tracing (command_msg "" tr ^ ": " ^ Timing.message timing_result)
         else ();
       val _ =
         if Timing.is_relevant timing_result