# HG changeset patch
# User wenzelm
# Date 1365514165 -7200
# Node ID 21c10672633b9096002c1ca949615bfddbbab5f6
# Parent  3db1bbc82d8da0685e28784b4b81fb7fce2472cb
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;

diff -r 3db1bbc82d8d -r 21c10672633b src/Doc/IsarImplementation/Integration.thy
--- a/src/Doc/IsarImplementation/Integration.thy	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy	Tue Apr 09 15:29:25 2013 +0200
@@ -145,7 +145,6 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
   Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.theory: "(theory -> theory) ->
@@ -166,10 +165,6 @@
   causes the toplevel loop to echo the result state (in interactive
   mode).
 
-  \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
-  transition should never show timing information, e.g.\ because it is
-  a diagnostic command.
-
   \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
   function.
 
diff -r 3db1bbc82d8d -r 21c10672633b src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -329,8 +329,7 @@
    Scan.succeed (boogie_status_vc false)) --
   vc_name >> (fn (f, vc_name) => f vc_name)
 
-fun status_cmd f = Toplevel.no_timing o Toplevel.keep (fn state =>
-  f (Toplevel.theory_of state))
+fun status_cmd f = Toplevel.keep (f o Toplevel.theory_of)
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "boogie_status"}
diff -r 3db1bbc82d8d -r 21c10672633b src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/HOL/Orderings.thy	Tue Apr 09 15:29:25 2013 +0200
@@ -492,8 +492,8 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_orders"}
     "print order structures available to transitivity reasoner"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-        Toplevel.keep (print_structures o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.unknown_context o
+      Toplevel.keep (print_structures o Toplevel.context_of)));
 
 end;
 
diff -r 3db1bbc82d8d -r 21c10672633b src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -81,10 +81,8 @@
 fun string_of_status NONE = "(unproved)"
   | string_of_status (SOME _) = "(proved)";
 
-fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state =>
+fun show_status thy (p, f) =
   let
-    val thy = Toplevel.theory_of state;
-
     val (context, defs, vcs) = SPARK_VCs.get_vcs thy true;
 
     val vcs' = AList.coalesce (op =) (map_filter
@@ -93,8 +91,7 @@
            SOME (trace, (name, status, ctxt, stmt))
          else NONE) vcs);
 
-    val ctxt = state |>
-      Toplevel.theory_of |>
+    val ctxt = thy |>
       Proof_Context.init_global |>
       Context.proof_map (fold Element.init context)
   in
@@ -116,7 +113,7 @@
            (Element.pretty_ctxt ctxt context' @
             Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
     Pretty.chunks2 |> Pretty.writeln
-  end);
+  end;
 
 val _ =
   Outer_Syntax.command @{command_spec "spark_open"}
@@ -165,7 +162,8 @@
        (Args.parens
           (   Args.$$$ "proved" >> K (is_some, K "")
            || Args.$$$ "unproved" >> K (is_none, K "")))
-       (K true, string_of_status) >> show_status);
+       (K true, string_of_status) >> (fn args =>
+        Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
 
 val _ =
   Outer_Syntax.command @{command_spec "spark_end"}
diff -r 3db1bbc82d8d -r 21c10672633b src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -123,9 +123,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
     "find theorems with (potentially) superfluous assumptions"
-    (Scan.option Parse.name
-      >> (fn opt_thy_name =>
-        Toplevel.no_timing o Toplevel.keep (fn state =>
-          print_unused_assms (Toplevel.context_of state) opt_thy_name)))
+    (Scan.option Parse.name >> (fn name =>
+      Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
 
 end
diff -r 3db1bbc82d8d -r 21c10672633b src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -249,7 +249,6 @@
   Outer_Syntax.improper_command @{command_spec "smt_status"}
     "show the available SMT solvers, the currently selected SMT solver, \
     \and the values of SMT configuration options"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
-      print_setup (Toplevel.context_of state))))
+    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
 
 end
diff -r 3db1bbc82d8d -r 21c10672633b src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -1175,8 +1175,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_inductives"}
     "print (co)inductive definitions and monotonicity rules"
-    (Scan.succeed
-      (Toplevel.no_timing o Toplevel.unknown_context o
-        Toplevel.keep (print_inductives o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.unknown_context o
+      Toplevel.keep (print_inductives o Toplevel.context_of)));
 
 end;
diff -r 3db1bbc82d8d -r 21c10672633b src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Provers/classical.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -968,9 +968,6 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-      Toplevel.keep (fn state =>
-        let val ctxt = Toplevel.context_of state
-        in print_claset ctxt end)));
+    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
 
 end;
diff -r 3db1bbc82d8d -r 21c10672633b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -281,7 +281,7 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
-    (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
+    (Parse.ML_source >> Isar_Cmd.ml_diag false);
 
 val _ =
   Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
@@ -381,7 +381,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_bundles"}
     "print bundles of declarations"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
 
 
@@ -746,197 +746,193 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
     "change default margin for pretty printing"
-    (Parse.nat >>
-      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
+    (Parse.nat >> (fn n => Toplevel.imperative (fn () => Pretty.margin_default := n)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "help"}
     "retrieve outer syntax commands according to name patterns"
-    (Scan.repeat Parse.name >> (fn pats =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
+    (Scan.repeat Parse.name >>
+      (fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
+    (Scan.succeed (Toplevel.imperative Outer_Syntax.print_outer_syntax));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_configs"} "print configuration options"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Attrib.print_configs o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.keep Toplevel.print_state_context));
+    (Scan.succeed (Toplevel.keep Toplevel.print_state_context));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theory"}
     "print logical theory contents (verbose!)"
-    (opt_bang >> (fn b => Toplevel.no_timing o Toplevel.unknown_theory o
+    (opt_bang >> (fn b => Toplevel.unknown_theory o
       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_syntax"}
     "print inner syntax of context (verbose!)"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_defn_rules"}
     "print definitional rewrite rules of context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
     "print constant abbreviations of context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theorems"}
     "print theorems of local theory or proof context"
-    (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
+    (opt_bang >> Isar_Cmd.print_theorems);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_locales"}
     "print locales of this theory"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+    (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_classes"}
     "print classes of this theory"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+    (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Class.print_classes o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_locale"}
     "print locale of this theory"
     (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
-      Toplevel.no_timing o Toplevel.unknown_theory o
+      Toplevel.unknown_theory o
       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_interps"}
     "print interpretations of locale for this theory or proof context"
-    (Parse.position Parse.xname >> (fn name => Toplevel.no_timing o Toplevel.unknown_context o
+    (Parse.position Parse.xname >> (fn name =>
+      Toplevel.unknown_context o
       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_dependencies"}
     "print dependencies of locale expression"
-    (opt_bang -- Parse_Spec.locale_expression true >> (fn (clean, expr) =>
-      Toplevel.no_timing o Toplevel.unknown_context o
-        Toplevel.keep (fn state =>
-          Expression.print_dependencies (Toplevel.context_of state) clean expr)));
+    (opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
+      Toplevel.unknown_context o
+      Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_attributes"}
     "print attributes of this theory"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+    (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_simpset"}
     "print context of Simplifier"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (fn state =>
         let val ctxt = Toplevel.context_of state
         in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+    (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
+    (Scan.succeed Isar_Cmd.thy_deps);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.locale_deps));
+    (Scan.succeed Isar_Cmd.locale_deps);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
+    (Scan.succeed Isar_Cmd.class_deps);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
-    (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
+    (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_statement"}
     "print theorems as long statements"
-    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
+    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_stmts);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
-    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
+    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_thms);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
-    (opt_modes -- Scan.option Parse_Spec.xthms1
-      >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
+    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs false);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
-    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
+    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs true);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
-    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
+    (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "term"} "read and print term"
-    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
+    (opt_modes -- Parse.term >> Isar_Cmd.print_term);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
     (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
-      >> (Toplevel.no_timing oo Isar_Cmd.print_type));
+      >> Isar_Cmd.print_type);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
-    (Scan.succeed
-      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
-        (Code.print_codesetup o Toplevel.theory_of)));
+    (Scan.succeed (Toplevel.unknown_theory o
+      Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
     (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
-       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
-         (Toplevel.no_timing oo Isar_Cmd.unused_thms));
+       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
 
 
 
@@ -944,44 +940,40 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "cd"} "change current working directory"
-    (Parse.path >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => File.cd (Path.explode name))));
+    (Parse.path >> (fn name => Toplevel.imperative (fn () => File.cd (Path.explode name))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "pwd"} "print current working directory"
-    (Scan.succeed (Toplevel.no_timing o
-      Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
+    (Scan.succeed (Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
-    (Parse.position Parse.name >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
+    (Parse.position Parse.name >>
+      (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database"
-    (Parse.name >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
+    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "kill_thy"}
     "kill theory -- try to remove from loader database"
-    (Parse.name >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
+    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "display_drafts"}
     "display raw source files with symbols"
-    (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
+    (Scan.repeat1 Parse.path >> Isar_Cmd.display_drafts);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_drafts"}
     "print raw source files with symbols"
-    (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
+    (Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
 
 val _ =  (* FIXME tty only *)
   Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
-      Toplevel.no_timing o Toplevel.keep (fn state =>
+      Toplevel.keep (fn state =>
        (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
         Toplevel.quiet := false;
         Print_Mode.with_modes modes (Toplevel.print_state true) state))));
@@ -989,32 +981,32 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "disable_pr"}
     "disable printing of toplevel state"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
+    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "enable_pr"}
     "enable printing of toplevel state"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
+    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "commit"}
     "commit current session to ML session image"
-    (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
+    (Parse.opt_unit >> K (Toplevel.imperative Secure.commit));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle"
-    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
+    (Parse.opt_unit >> (K (Toplevel.imperative quit)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop"
     (Scan.succeed
-      (Toplevel.no_timing o Toplevel.keep (fn state =>
+      (Toplevel.keep (fn state =>
         (Context.set_thread_data (try Toplevel.generic_theory_of state);
           raise Runtime.TERMINATE))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o Session.welcome)));
+    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
 
 
 
@@ -1022,22 +1014,22 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
+    (Scan.succeed (Toplevel.imperative Isar.init));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
     (Scan.optional Parse.nat 1 >>
-      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n)));
+      (fn n => Toplevel.imperative (fn () => Isar.linear_undo n)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
     (Scan.optional Parse.nat 1 >>
-      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));
+      (fn n => Toplevel.imperative (fn () => Isar.undo n)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "undos_proof"}
     "undo commands (skipping closed proofs)"
-    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
+    (Scan.optional Parse.nat 1 >> (fn n =>
       Toplevel.keep (fn state =>
         if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
 
@@ -1045,13 +1037,13 @@
   Outer_Syntax.improper_command @{command_spec "cannot_undo"}
     "partial undo -- Proof General legacy"
     (Parse.name >>
-      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)
+      (fn "end" => Toplevel.imperative (fn () => Isar.undo 1)
         | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "kill"}
     "kill partial proof or theory development"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill));
+    (Scan.succeed (Toplevel.imperative Isar.kill));
 
 
 
diff -r 3db1bbc82d8d -r 21c10672633b 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
diff -r 3db1bbc82d8d -r 21c10672633b src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -193,37 +193,34 @@
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
+    (Scan.succeed (Toplevel.keep (fn state =>
       if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
       else (Toplevel.quiet := false; Toplevel.print_state true state))));
 
 val _ = (*undo without output -- historical*)
   Outer_Syntax.improper_command
     (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
+    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
 
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)"
-    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
+    (Parse.opt_unit >> (K (Toplevel.imperative restart)));
 
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)"
-    (Scan.succeed (Toplevel.no_timing o
-      Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
+    (Scan.succeed (Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)"
-    (Parse.name >> (fn file =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
+    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_processed file)));
 
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)"
-    (Parse.name >> (Toplevel.no_timing oo
-      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
+    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file)));
 
 
 (* init *)
diff -r 3db1bbc82d8d -r 21c10672633b src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -1031,10 +1031,10 @@
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
-    (Parse.text >> (Toplevel.no_timing oo
+    (Parse.text >>
       (fn txt => Toplevel.imperative (fn () =>
         if print_mode_active proof_general_emacsN
         then process_pgip_emacs txt
-        else process_pgip_plain txt))));
+        else process_pgip_plain txt)));
 
 end;
diff -r 3db1bbc82d8d -r 21c10672633b src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Pure/Tools/find_consts.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -139,8 +139,7 @@
   Outer_Syntax.improper_command @{command_spec "find_consts"}
     "find constants by name/type patterns"
     (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
-      >> (fn spec => Toplevel.no_timing o
-        Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
+      >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
 
 end;
 
diff -r 3db1bbc82d8d -r 21c10672633b src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -628,7 +628,6 @@
     "find theorems meeting specified criteria"
     (options -- query_parser
       >> (fn ((opt_lim, rem_dups), spec) =>
-        Toplevel.no_timing o
         Toplevel.keep (fn state =>
           let
             val ctxt = Toplevel.context_of state;
diff -r 3db1bbc82d8d -r 21c10672633b src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -505,8 +505,7 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
-    (Scan.succeed
-      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
-        (print_codeproc o Toplevel.theory_of)));
+    (Scan.succeed (Toplevel.unknown_theory o
+      Toplevel.keep (print_codeproc o Toplevel.theory_of)));
 
 end; (*struct*)
diff -r 3db1bbc82d8d -r 21c10672633b src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -1058,16 +1058,16 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "code_thms"}
     "print system of code equations for code"
-    (Scan.repeat1 Parse.term_group
-      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
-        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
+    (Scan.repeat1 Parse.term_group >> (fn cs =>
+      Toplevel.unknown_theory o
+      Toplevel.keep (fn state => code_thms_cmd (Toplevel.theory_of state) cs)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "code_deps"}
     "visualize dependencies of code equations for code"
-    (Scan.repeat1 Parse.term_group
-      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
-        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
+    (Scan.repeat1 Parse.term_group >> (fn cs =>
+      Toplevel.unknown_theory o
+      Toplevel.keep (fn state => code_deps_cmd (Toplevel.theory_of state) cs)));
 
 end;
 
diff -r 3db1bbc82d8d -r 21c10672633b src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Tools/induct.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -261,7 +261,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
     "print induction and cases rules"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_rules o Toplevel.context_of)));
 
 
diff -r 3db1bbc82d8d -r 21c10672633b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Tools/quickcheck.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -533,7 +533,7 @@
   Outer_Syntax.improper_command @{command_spec "quickcheck"}
     "try to find counterexample for subgoal"
     (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
-      Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
+      Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
 
 
 (* automatic testing *)
diff -r 3db1bbc82d8d -r 21c10672633b src/Tools/value.ML
--- a/src/Tools/value.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Tools/value.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -65,8 +65,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
     (opt_evaluator -- opt_modes -- Parse.term
-      >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
-          (value_cmd some_name modes t)));
+      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
 
 val antiq_setup =
   Thy_Output.antiquotation @{binding value}
diff -r 3db1bbc82d8d -r 21c10672633b src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/ZF/Tools/typechk.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -122,7 +122,7 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_tcset o Toplevel.context_of)));