discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
authorwenzelm
Tue Apr 09 15:29:25 2013 +0200 (2013-04-09)
changeset 5165821c10672633b
parent 51657 3db1bbc82d8d
child 51659 5151706dc9a6
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;
src/Doc/IsarImplementation/Integration.thy
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Orderings.thy
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Tools/Quickcheck/find_unused_assms.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/inductive.ML
src/Provers/classical.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/toplevel.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
src/Tools/induct.ML
src/Tools/quickcheck.ML
src/Tools/value.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/Doc/IsarImplementation/Integration.thy	Tue Apr 09 13:55:28 2013 +0200
     1.2 +++ b/src/Doc/IsarImplementation/Integration.thy	Tue Apr 09 15:29:25 2013 +0200
     1.3 @@ -145,7 +145,6 @@
     1.4  text %mlref {*
     1.5    \begin{mldecls}
     1.6    @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
     1.7 -  @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
     1.8    @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
     1.9    Toplevel.transition -> Toplevel.transition"} \\
    1.10    @{index_ML Toplevel.theory: "(theory -> theory) ->
    1.11 @@ -166,10 +165,6 @@
    1.12    causes the toplevel loop to echo the result state (in interactive
    1.13    mode).
    1.14  
    1.15 -  \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
    1.16 -  transition should never show timing information, e.g.\ because it is
    1.17 -  a diagnostic command.
    1.18 -
    1.19    \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
    1.20    function.
    1.21  
     2.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Apr 09 13:55:28 2013 +0200
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Apr 09 15:29:25 2013 +0200
     2.3 @@ -329,8 +329,7 @@
     2.4     Scan.succeed (boogie_status_vc false)) --
     2.5    vc_name >> (fn (f, vc_name) => f vc_name)
     2.6  
     2.7 -fun status_cmd f = Toplevel.no_timing o Toplevel.keep (fn state =>
     2.8 -  f (Toplevel.theory_of state))
     2.9 +fun status_cmd f = Toplevel.keep (f o Toplevel.theory_of)
    2.10  
    2.11  val _ =
    2.12    Outer_Syntax.improper_command @{command_spec "boogie_status"}
     3.1 --- a/src/HOL/Orderings.thy	Tue Apr 09 13:55:28 2013 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Tue Apr 09 15:29:25 2013 +0200
     3.3 @@ -492,8 +492,8 @@
     3.4  val _ =
     3.5    Outer_Syntax.improper_command @{command_spec "print_orders"}
     3.6      "print order structures available to transitivity reasoner"
     3.7 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
     3.8 -        Toplevel.keep (print_structures o Toplevel.context_of)));
     3.9 +    (Scan.succeed (Toplevel.unknown_context o
    3.10 +      Toplevel.keep (print_structures o Toplevel.context_of)));
    3.11  
    3.12  end;
    3.13  
     4.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Tue Apr 09 13:55:28 2013 +0200
     4.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Tue Apr 09 15:29:25 2013 +0200
     4.3 @@ -81,10 +81,8 @@
     4.4  fun string_of_status NONE = "(unproved)"
     4.5    | string_of_status (SOME _) = "(proved)";
     4.6  
     4.7 -fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state =>
     4.8 +fun show_status thy (p, f) =
     4.9    let
    4.10 -    val thy = Toplevel.theory_of state;
    4.11 -
    4.12      val (context, defs, vcs) = SPARK_VCs.get_vcs thy true;
    4.13  
    4.14      val vcs' = AList.coalesce (op =) (map_filter
    4.15 @@ -93,8 +91,7 @@
    4.16             SOME (trace, (name, status, ctxt, stmt))
    4.17           else NONE) vcs);
    4.18  
    4.19 -    val ctxt = state |>
    4.20 -      Toplevel.theory_of |>
    4.21 +    val ctxt = thy |>
    4.22        Proof_Context.init_global |>
    4.23        Context.proof_map (fold Element.init context)
    4.24    in
    4.25 @@ -116,7 +113,7 @@
    4.26             (Element.pretty_ctxt ctxt context' @
    4.27              Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
    4.28      Pretty.chunks2 |> Pretty.writeln
    4.29 -  end);
    4.30 +  end;
    4.31  
    4.32  val _ =
    4.33    Outer_Syntax.command @{command_spec "spark_open"}
    4.34 @@ -165,7 +162,8 @@
    4.35         (Args.parens
    4.36            (   Args.$$$ "proved" >> K (is_some, K "")
    4.37             || Args.$$$ "unproved" >> K (is_none, K "")))
    4.38 -       (K true, string_of_status) >> show_status);
    4.39 +       (K true, string_of_status) >> (fn args =>
    4.40 +        Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
    4.41  
    4.42  val _ =
    4.43    Outer_Syntax.command @{command_spec "spark_end"}
     5.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Apr 09 13:55:28 2013 +0200
     5.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Apr 09 15:29:25 2013 +0200
     5.3 @@ -123,9 +123,7 @@
     5.4  val _ =
     5.5    Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
     5.6      "find theorems with (potentially) superfluous assumptions"
     5.7 -    (Scan.option Parse.name
     5.8 -      >> (fn opt_thy_name =>
     5.9 -        Toplevel.no_timing o Toplevel.keep (fn state =>
    5.10 -          print_unused_assms (Toplevel.context_of state) opt_thy_name)))
    5.11 +    (Scan.option Parse.name >> (fn name =>
    5.12 +      Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
    5.13  
    5.14  end
     6.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Tue Apr 09 13:55:28 2013 +0200
     6.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Apr 09 15:29:25 2013 +0200
     6.3 @@ -249,7 +249,6 @@
     6.4    Outer_Syntax.improper_command @{command_spec "smt_status"}
     6.5      "show the available SMT solvers, the currently selected SMT solver, \
     6.6      \and the values of SMT configuration options"
     6.7 -    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
     6.8 -      print_setup (Toplevel.context_of state))))
     6.9 +    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
    6.10  
    6.11  end
     7.1 --- a/src/HOL/Tools/inductive.ML	Tue Apr 09 13:55:28 2013 +0200
     7.2 +++ b/src/HOL/Tools/inductive.ML	Tue Apr 09 15:29:25 2013 +0200
     7.3 @@ -1175,8 +1175,7 @@
     7.4  val _ =
     7.5    Outer_Syntax.improper_command @{command_spec "print_inductives"}
     7.6      "print (co)inductive definitions and monotonicity rules"
     7.7 -    (Scan.succeed
     7.8 -      (Toplevel.no_timing o Toplevel.unknown_context o
     7.9 -        Toplevel.keep (print_inductives o Toplevel.context_of)));
    7.10 +    (Scan.succeed (Toplevel.unknown_context o
    7.11 +      Toplevel.keep (print_inductives o Toplevel.context_of)));
    7.12  
    7.13  end;
     8.1 --- a/src/Provers/classical.ML	Tue Apr 09 13:55:28 2013 +0200
     8.2 +++ b/src/Provers/classical.ML	Tue Apr 09 15:29:25 2013 +0200
     8.3 @@ -968,9 +968,6 @@
     8.4  
     8.5  val _ =
     8.6    Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
     8.7 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
     8.8 -      Toplevel.keep (fn state =>
     8.9 -        let val ctxt = Toplevel.context_of state
    8.10 -        in print_claset ctxt end)));
    8.11 +    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
    8.12  
    8.13  end;
     9.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Apr 09 13:55:28 2013 +0200
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 09 15:29:25 2013 +0200
     9.3 @@ -281,7 +281,7 @@
     9.4  
     9.5  val _ =
     9.6    Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
     9.7 -    (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
     9.8 +    (Parse.ML_source >> Isar_Cmd.ml_diag false);
     9.9  
    9.10  val _ =
    9.11    Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
    9.12 @@ -381,7 +381,7 @@
    9.13  val _ =
    9.14    Outer_Syntax.improper_command @{command_spec "print_bundles"}
    9.15      "print bundles of declarations"
    9.16 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    9.17 +    (Scan.succeed (Toplevel.unknown_context o
    9.18        Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
    9.19  
    9.20  
    9.21 @@ -746,197 +746,193 @@
    9.22  val _ =
    9.23    Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
    9.24      "change default margin for pretty printing"
    9.25 -    (Parse.nat >>
    9.26 -      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
    9.27 +    (Parse.nat >> (fn n => Toplevel.imperative (fn () => Pretty.margin_default := n)));
    9.28  
    9.29  val _ =
    9.30    Outer_Syntax.improper_command @{command_spec "help"}
    9.31      "retrieve outer syntax commands according to name patterns"
    9.32 -    (Scan.repeat Parse.name >> (fn pats =>
    9.33 -      Toplevel.no_timing o Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
    9.34 +    (Scan.repeat Parse.name >>
    9.35 +      (fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
    9.36  
    9.37  val _ =
    9.38    Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
    9.39 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
    9.40 +    (Scan.succeed (Toplevel.imperative Outer_Syntax.print_outer_syntax));
    9.41  
    9.42  val _ =
    9.43    Outer_Syntax.improper_command @{command_spec "print_configs"} "print configuration options"
    9.44 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    9.45 +    (Scan.succeed (Toplevel.unknown_context o
    9.46        Toplevel.keep (Attrib.print_configs o Toplevel.context_of)));
    9.47  
    9.48  val _ =
    9.49    Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
    9.50 -    (Scan.succeed (Toplevel.no_timing o Toplevel.keep Toplevel.print_state_context));
    9.51 +    (Scan.succeed (Toplevel.keep Toplevel.print_state_context));
    9.52  
    9.53  val _ =
    9.54    Outer_Syntax.improper_command @{command_spec "print_theory"}
    9.55      "print logical theory contents (verbose!)"
    9.56 -    (opt_bang >> (fn b => Toplevel.no_timing o Toplevel.unknown_theory o
    9.57 +    (opt_bang >> (fn b => Toplevel.unknown_theory o
    9.58        Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
    9.59  
    9.60  val _ =
    9.61    Outer_Syntax.improper_command @{command_spec "print_syntax"}
    9.62      "print inner syntax of context (verbose!)"
    9.63 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    9.64 +    (Scan.succeed (Toplevel.unknown_context o
    9.65        Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
    9.66  
    9.67  val _ =
    9.68    Outer_Syntax.improper_command @{command_spec "print_defn_rules"}
    9.69      "print definitional rewrite rules of context"
    9.70 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    9.71 +    (Scan.succeed (Toplevel.unknown_context o
    9.72        Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
    9.73  
    9.74  val _ =
    9.75    Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
    9.76      "print constant abbreviations of context"
    9.77 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    9.78 +    (Scan.succeed (Toplevel.unknown_context o
    9.79        Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
    9.80  
    9.81  val _ =
    9.82    Outer_Syntax.improper_command @{command_spec "print_theorems"}
    9.83      "print theorems of local theory or proof context"
    9.84 -    (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
    9.85 +    (opt_bang >> Isar_Cmd.print_theorems);
    9.86  
    9.87  val _ =
    9.88    Outer_Syntax.improper_command @{command_spec "print_locales"}
    9.89      "print locales of this theory"
    9.90 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    9.91 +    (Scan.succeed (Toplevel.unknown_theory o
    9.92        Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
    9.93  
    9.94  val _ =
    9.95    Outer_Syntax.improper_command @{command_spec "print_classes"}
    9.96      "print classes of this theory"
    9.97 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    9.98 +    (Scan.succeed (Toplevel.unknown_theory o
    9.99        Toplevel.keep (Class.print_classes o Toplevel.context_of)));
   9.100  
   9.101  val _ =
   9.102    Outer_Syntax.improper_command @{command_spec "print_locale"}
   9.103      "print locale of this theory"
   9.104      (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
   9.105 -      Toplevel.no_timing o Toplevel.unknown_theory o
   9.106 +      Toplevel.unknown_theory o
   9.107        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
   9.108  
   9.109  val _ =
   9.110    Outer_Syntax.improper_command @{command_spec "print_interps"}
   9.111      "print interpretations of locale for this theory or proof context"
   9.112 -    (Parse.position Parse.xname >> (fn name => Toplevel.no_timing o Toplevel.unknown_context o
   9.113 +    (Parse.position Parse.xname >> (fn name =>
   9.114 +      Toplevel.unknown_context o
   9.115        Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
   9.116  
   9.117  val _ =
   9.118    Outer_Syntax.improper_command @{command_spec "print_dependencies"}
   9.119      "print dependencies of locale expression"
   9.120 -    (opt_bang -- Parse_Spec.locale_expression true >> (fn (clean, expr) =>
   9.121 -      Toplevel.no_timing o Toplevel.unknown_context o
   9.122 -        Toplevel.keep (fn state =>
   9.123 -          Expression.print_dependencies (Toplevel.context_of state) clean expr)));
   9.124 +    (opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
   9.125 +      Toplevel.unknown_context o
   9.126 +      Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
   9.127  
   9.128  val _ =
   9.129    Outer_Syntax.improper_command @{command_spec "print_attributes"}
   9.130      "print attributes of this theory"
   9.131 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   9.132 +    (Scan.succeed (Toplevel.unknown_theory o
   9.133        Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of)));
   9.134  
   9.135  val _ =
   9.136    Outer_Syntax.improper_command @{command_spec "print_simpset"}
   9.137      "print context of Simplifier"
   9.138 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   9.139 +    (Scan.succeed (Toplevel.unknown_context o
   9.140        Toplevel.keep (fn state =>
   9.141          let val ctxt = Toplevel.context_of state
   9.142          in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end)));
   9.143  
   9.144  val _ =
   9.145    Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules"
   9.146 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   9.147 +    (Scan.succeed (Toplevel.unknown_context o
   9.148        Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
   9.149  
   9.150  val _ =
   9.151    Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
   9.152 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   9.153 +    (Scan.succeed (Toplevel.unknown_context o
   9.154        Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
   9.155  
   9.156  val _ =
   9.157    Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
   9.158 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   9.159 +    (Scan.succeed (Toplevel.unknown_theory o
   9.160        Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
   9.161  
   9.162  val _ =
   9.163    Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
   9.164 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   9.165 +    (Scan.succeed (Toplevel.unknown_context o
   9.166        Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
   9.167  
   9.168  val _ =
   9.169    Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
   9.170 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
   9.171 +    (Scan.succeed Isar_Cmd.thy_deps);
   9.172  
   9.173  val _ =
   9.174    Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
   9.175 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.locale_deps));
   9.176 +    (Scan.succeed Isar_Cmd.locale_deps);
   9.177  
   9.178  val _ =
   9.179    Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
   9.180 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
   9.181 +    (Scan.succeed Isar_Cmd.class_deps);
   9.182  
   9.183  val _ =
   9.184    Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
   9.185 -    (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
   9.186 +    (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
   9.187  
   9.188  val _ =
   9.189    Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
   9.190 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   9.191 +    (Scan.succeed (Toplevel.unknown_context o
   9.192        Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
   9.193  
   9.194  val _ =
   9.195    Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
   9.196 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   9.197 +    (Scan.succeed (Toplevel.unknown_context o
   9.198        Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of)));
   9.199  
   9.200  val _ =
   9.201    Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
   9.202 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   9.203 +    (Scan.succeed (Toplevel.unknown_context o
   9.204        Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
   9.205  
   9.206  val _ =
   9.207    Outer_Syntax.improper_command @{command_spec "print_statement"}
   9.208      "print theorems as long statements"
   9.209 -    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
   9.210 +    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_stmts);
   9.211  
   9.212  val _ =
   9.213    Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
   9.214 -    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
   9.215 +    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_thms);
   9.216  
   9.217  val _ =
   9.218    Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
   9.219 -    (opt_modes -- Scan.option Parse_Spec.xthms1
   9.220 -      >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
   9.221 +    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs false);
   9.222  
   9.223  val _ =
   9.224    Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
   9.225 -    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
   9.226 +    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs true);
   9.227  
   9.228  val _ =
   9.229    Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
   9.230 -    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
   9.231 +    (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
   9.232  
   9.233  val _ =
   9.234    Outer_Syntax.improper_command @{command_spec "term"} "read and print term"
   9.235 -    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
   9.236 +    (opt_modes -- Parse.term >> Isar_Cmd.print_term);
   9.237  
   9.238  val _ =
   9.239    Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
   9.240      (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
   9.241 -      >> (Toplevel.no_timing oo Isar_Cmd.print_type));
   9.242 +      >> Isar_Cmd.print_type);
   9.243  
   9.244  val _ =
   9.245    Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
   9.246 -    (Scan.succeed
   9.247 -      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
   9.248 -        (Code.print_codesetup o Toplevel.theory_of)));
   9.249 +    (Scan.succeed (Toplevel.unknown_theory o
   9.250 +      Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
   9.251  
   9.252  val _ =
   9.253    Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
   9.254      (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
   9.255 -       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
   9.256 -         (Toplevel.no_timing oo Isar_Cmd.unused_thms));
   9.257 +       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
   9.258  
   9.259  
   9.260  
   9.261 @@ -944,44 +940,40 @@
   9.262  
   9.263  val _ =
   9.264    Outer_Syntax.improper_command @{command_spec "cd"} "change current working directory"
   9.265 -    (Parse.path >> (fn name =>
   9.266 -      Toplevel.no_timing o Toplevel.imperative (fn () => File.cd (Path.explode name))));
   9.267 +    (Parse.path >> (fn name => Toplevel.imperative (fn () => File.cd (Path.explode name))));
   9.268  
   9.269  val _ =
   9.270    Outer_Syntax.improper_command @{command_spec "pwd"} "print current working directory"
   9.271 -    (Scan.succeed (Toplevel.no_timing o
   9.272 -      Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
   9.273 +    (Scan.succeed (Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
   9.274  
   9.275  val _ =
   9.276    Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
   9.277 -    (Parse.position Parse.name >> (fn name =>
   9.278 -      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
   9.279 +    (Parse.position Parse.name >>
   9.280 +      (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
   9.281  
   9.282  val _ =
   9.283    Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database"
   9.284 -    (Parse.name >> (fn name =>
   9.285 -      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
   9.286 +    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
   9.287  
   9.288  val _ =
   9.289    Outer_Syntax.improper_command @{command_spec "kill_thy"}
   9.290      "kill theory -- try to remove from loader database"
   9.291 -    (Parse.name >> (fn name =>
   9.292 -      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
   9.293 +    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
   9.294  
   9.295  val _ =
   9.296    Outer_Syntax.improper_command @{command_spec "display_drafts"}
   9.297      "display raw source files with symbols"
   9.298 -    (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
   9.299 +    (Scan.repeat1 Parse.path >> Isar_Cmd.display_drafts);
   9.300  
   9.301  val _ =
   9.302    Outer_Syntax.improper_command @{command_spec "print_drafts"}
   9.303      "print raw source files with symbols"
   9.304 -    (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
   9.305 +    (Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
   9.306  
   9.307  val _ =  (* FIXME tty only *)
   9.308    Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
   9.309      (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
   9.310 -      Toplevel.no_timing o Toplevel.keep (fn state =>
   9.311 +      Toplevel.keep (fn state =>
   9.312         (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
   9.313          Toplevel.quiet := false;
   9.314          Print_Mode.with_modes modes (Toplevel.print_state true) state))));
   9.315 @@ -989,32 +981,32 @@
   9.316  val _ =
   9.317    Outer_Syntax.improper_command @{command_spec "disable_pr"}
   9.318      "disable printing of toplevel state"
   9.319 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
   9.320 +    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
   9.321  
   9.322  val _ =
   9.323    Outer_Syntax.improper_command @{command_spec "enable_pr"}
   9.324      "enable printing of toplevel state"
   9.325 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
   9.326 +    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
   9.327  
   9.328  val _ =
   9.329    Outer_Syntax.improper_command @{command_spec "commit"}
   9.330      "commit current session to ML session image"
   9.331 -    (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
   9.332 +    (Parse.opt_unit >> K (Toplevel.imperative Secure.commit));
   9.333  
   9.334  val _ =
   9.335    Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle"
   9.336 -    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
   9.337 +    (Parse.opt_unit >> (K (Toplevel.imperative quit)));
   9.338  
   9.339  val _ =
   9.340    Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop"
   9.341      (Scan.succeed
   9.342 -      (Toplevel.no_timing o Toplevel.keep (fn state =>
   9.343 +      (Toplevel.keep (fn state =>
   9.344          (Context.set_thread_data (try Toplevel.generic_theory_of state);
   9.345            raise Runtime.TERMINATE))));
   9.346  
   9.347  val _ =
   9.348    Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
   9.349 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o Session.welcome)));
   9.350 +    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
   9.351  
   9.352  
   9.353  
   9.354 @@ -1022,22 +1014,22 @@
   9.355  
   9.356  val _ =
   9.357    Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
   9.358 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
   9.359 +    (Scan.succeed (Toplevel.imperative Isar.init));
   9.360  
   9.361  val _ =
   9.362    Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
   9.363      (Scan.optional Parse.nat 1 >>
   9.364 -      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n)));
   9.365 +      (fn n => Toplevel.imperative (fn () => Isar.linear_undo n)));
   9.366  
   9.367  val _ =
   9.368    Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
   9.369      (Scan.optional Parse.nat 1 >>
   9.370 -      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));
   9.371 +      (fn n => Toplevel.imperative (fn () => Isar.undo n)));
   9.372  
   9.373  val _ =
   9.374    Outer_Syntax.improper_command @{command_spec "undos_proof"}
   9.375      "undo commands (skipping closed proofs)"
   9.376 -    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
   9.377 +    (Scan.optional Parse.nat 1 >> (fn n =>
   9.378        Toplevel.keep (fn state =>
   9.379          if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
   9.380  
   9.381 @@ -1045,13 +1037,13 @@
   9.382    Outer_Syntax.improper_command @{command_spec "cannot_undo"}
   9.383      "partial undo -- Proof General legacy"
   9.384      (Parse.name >>
   9.385 -      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)
   9.386 +      (fn "end" => Toplevel.imperative (fn () => Isar.undo 1)
   9.387          | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
   9.388  
   9.389  val _ =
   9.390    Outer_Syntax.improper_command @{command_spec "kill"}
   9.391      "kill partial proof or theory development"
   9.392 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill));
   9.393 +    (Scan.succeed (Toplevel.imperative Isar.kill));
   9.394  
   9.395  
   9.396  
    10.1 --- a/src/Pure/Isar/toplevel.ML	Tue Apr 09 13:55:28 2013 +0200
    10.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Apr 09 15:29:25 2013 +0200
    10.3 @@ -42,7 +42,6 @@
    10.4    val interactive: bool -> transition -> transition
    10.5    val set_print: bool -> transition -> transition
    10.6    val print: transition -> transition
    10.7 -  val no_timing: transition -> transition
    10.8    val init_theory: (unit -> theory) -> transition -> transition
    10.9    val is_init: transition -> bool
   10.10    val modify_init: (unit -> theory) -> transition -> transition
   10.11 @@ -346,18 +345,17 @@
   10.12    pos: Position.T,           (*source position*)
   10.13    int_only: bool,            (*interactive-only*)
   10.14    print: bool,               (*print result state*)
   10.15 -  no_timing: bool,           (*suppress timing*)
   10.16    timing: Time.time option,  (*prescient timing information*)
   10.17    trans: trans list};        (*primitive transitions (union)*)
   10.18  
   10.19 -fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
   10.20 +fun make_transition (name, pos, int_only, print, timing, trans) =
   10.21    Transition {name = name, pos = pos, int_only = int_only, print = print,
   10.22 -    no_timing = no_timing, timing = timing, trans = trans};
   10.23 +    timing = timing, trans = trans};
   10.24  
   10.25 -fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
   10.26 -  make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
   10.27 +fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) =
   10.28 +  make_transition (f (name, pos, int_only, print, timing, trans));
   10.29  
   10.30 -val empty = make_transition ("", Position.none, false, false, false, NONE, []);
   10.31 +val empty = make_transition ("", Position.none, false, false, NONE, []);
   10.32  
   10.33  
   10.34  (* diagnostics *)
   10.35 @@ -375,26 +373,23 @@
   10.36  
   10.37  (* modify transitions *)
   10.38  
   10.39 -fun name name = map_transition (fn (_, pos, int_only, print, no_timing, timing, trans) =>
   10.40 -  (name, pos, int_only, print, no_timing, timing, trans));
   10.41 +fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) =>
   10.42 +  (name, pos, int_only, print, timing, trans));
   10.43  
   10.44 -fun position pos = map_transition (fn (name, _, int_only, print, no_timing, timing, trans) =>
   10.45 -  (name, pos, int_only, print, no_timing, timing, trans));
   10.46 +fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) =>
   10.47 +  (name, pos, int_only, print, timing, trans));
   10.48  
   10.49 -fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, timing, trans) =>
   10.50 -  (name, pos, int_only, print, no_timing, timing, trans));
   10.51 +fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) =>
   10.52 +  (name, pos, int_only, print, timing, trans));
   10.53  
   10.54 -val no_timing = map_transition (fn (name, pos, int_only, print, _, timing, trans) =>
   10.55 -  (name, pos, int_only, print, true, timing, trans));
   10.56 -
   10.57 -fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, timing, trans) =>
   10.58 -  (name, pos, int_only, print, no_timing, timing, tr :: trans));
   10.59 +fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) =>
   10.60 +  (name, pos, int_only, print, timing, tr :: trans));
   10.61  
   10.62 -val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, timing, _) =>
   10.63 -  (name, pos, int_only, print, no_timing, timing, []));
   10.64 +val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) =>
   10.65 +  (name, pos, int_only, print, timing, []));
   10.66  
   10.67 -fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, timing, trans) =>
   10.68 -  (name, pos, int_only, print, no_timing, timing, trans));
   10.69 +fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) =>
   10.70 +  (name, pos, int_only, print, timing, trans));
   10.71  
   10.72  val print = set_print true;
   10.73  
   10.74 @@ -633,28 +628,26 @@
   10.75  (* apply transitions *)
   10.76  
   10.77  fun get_timing (Transition {timing, ...}) = timing;
   10.78 -fun put_timing timing = map_transition (fn (name, pos, int_only, print, no_timing, _, trans) =>
   10.79 -  (name, pos, int_only, print, no_timing, timing, trans));
   10.80 +fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
   10.81 +  (name, pos, int_only, print, timing, trans));
   10.82  
   10.83  local
   10.84  
   10.85 -fun app int (tr as Transition {trans, print, no_timing, ...}) =
   10.86 +fun app int (tr as Transition {trans, print, ...}) =
   10.87    setmp_thread_position tr (fn state =>
   10.88      let
   10.89        val timing_start = Timing.start ();
   10.90  
   10.91        val (result, opt_err) =
   10.92 -         state |>
   10.93 -          (apply_trans int trans
   10.94 -            |> (! profiling > 0 andalso not no_timing) ? profile (! profiling));
   10.95 +         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
   10.96        val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
   10.97  
   10.98        val timing_result = Timing.result timing_start;
   10.99  
  10.100        val _ =
  10.101 -        if Timing.is_relevant timing_result andalso
  10.102 -          (! profiling > 0 orelse ! timing andalso not no_timing)
  10.103 -        then warning (command_msg "" tr ^ ": " ^ Timing.message timing_result)
  10.104 +        if Timing.is_relevant timing_result andalso (! profiling > 0 orelse ! timing)
  10.105 +          andalso not (Keyword.is_control (name_of tr))
  10.106 +        then tracing (command_msg "" tr ^ ": " ^ Timing.message timing_result)
  10.107          else ();
  10.108        val _ =
  10.109          if Timing.is_relevant timing_result
    11.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Apr 09 13:55:28 2013 +0200
    11.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Apr 09 15:29:25 2013 +0200
    11.3 @@ -193,37 +193,34 @@
    11.4  val _ =
    11.5    Outer_Syntax.improper_command
    11.6      (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)"
    11.7 -    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
    11.8 +    (Scan.succeed (Toplevel.keep (fn state =>
    11.9        if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
   11.10        else (Toplevel.quiet := false; Toplevel.print_state true state))));
   11.11  
   11.12  val _ = (*undo without output -- historical*)
   11.13    Outer_Syntax.improper_command
   11.14      (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)"
   11.15 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
   11.16 +    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
   11.17  
   11.18  val _ =
   11.19    Outer_Syntax.improper_command
   11.20      (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)"
   11.21 -    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
   11.22 +    (Parse.opt_unit >> (K (Toplevel.imperative restart)));
   11.23  
   11.24  val _ =
   11.25    Outer_Syntax.improper_command
   11.26      (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)"
   11.27 -    (Scan.succeed (Toplevel.no_timing o
   11.28 -      Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
   11.29 +    (Scan.succeed (Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
   11.30  
   11.31  val _ =
   11.32    Outer_Syntax.improper_command
   11.33      (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)"
   11.34 -    (Parse.name >> (fn file =>
   11.35 -      Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
   11.36 +    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_processed file)));
   11.37  
   11.38  val _ =
   11.39    Outer_Syntax.improper_command
   11.40      (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)"
   11.41 -    (Parse.name >> (Toplevel.no_timing oo
   11.42 -      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
   11.43 +    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file)));
   11.44  
   11.45  
   11.46  (* init *)
    12.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Apr 09 13:55:28 2013 +0200
    12.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Apr 09 15:29:25 2013 +0200
    12.3 @@ -1031,10 +1031,10 @@
    12.4  val _ =
    12.5    Outer_Syntax.improper_command
    12.6      (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
    12.7 -    (Parse.text >> (Toplevel.no_timing oo
    12.8 +    (Parse.text >>
    12.9        (fn txt => Toplevel.imperative (fn () =>
   12.10          if print_mode_active proof_general_emacsN
   12.11          then process_pgip_emacs txt
   12.12 -        else process_pgip_plain txt))));
   12.13 +        else process_pgip_plain txt)));
   12.14  
   12.15  end;
    13.1 --- a/src/Pure/Tools/find_consts.ML	Tue Apr 09 13:55:28 2013 +0200
    13.2 +++ b/src/Pure/Tools/find_consts.ML	Tue Apr 09 15:29:25 2013 +0200
    13.3 @@ -139,8 +139,7 @@
    13.4    Outer_Syntax.improper_command @{command_spec "find_consts"}
    13.5      "find constants by name/type patterns"
    13.6      (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
    13.7 -      >> (fn spec => Toplevel.no_timing o
    13.8 -        Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
    13.9 +      >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
   13.10  
   13.11  end;
   13.12  
    14.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Apr 09 13:55:28 2013 +0200
    14.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Apr 09 15:29:25 2013 +0200
    14.3 @@ -628,7 +628,6 @@
    14.4      "find theorems meeting specified criteria"
    14.5      (options -- query_parser
    14.6        >> (fn ((opt_lim, rem_dups), spec) =>
    14.7 -        Toplevel.no_timing o
    14.8          Toplevel.keep (fn state =>
    14.9            let
   14.10              val ctxt = Toplevel.context_of state;
    15.1 --- a/src/Tools/Code/code_preproc.ML	Tue Apr 09 13:55:28 2013 +0200
    15.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Apr 09 15:29:25 2013 +0200
    15.3 @@ -505,8 +505,7 @@
    15.4  
    15.5  val _ =
    15.6    Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
    15.7 -    (Scan.succeed
    15.8 -      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
    15.9 -        (print_codeproc o Toplevel.theory_of)));
   15.10 +    (Scan.succeed (Toplevel.unknown_theory o
   15.11 +      Toplevel.keep (print_codeproc o Toplevel.theory_of)));
   15.12  
   15.13  end; (*struct*)
    16.1 --- a/src/Tools/Code/code_thingol.ML	Tue Apr 09 13:55:28 2013 +0200
    16.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Apr 09 15:29:25 2013 +0200
    16.3 @@ -1058,16 +1058,16 @@
    16.4  val _ =
    16.5    Outer_Syntax.improper_command @{command_spec "code_thms"}
    16.6      "print system of code equations for code"
    16.7 -    (Scan.repeat1 Parse.term_group
    16.8 -      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    16.9 -        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
   16.10 +    (Scan.repeat1 Parse.term_group >> (fn cs =>
   16.11 +      Toplevel.unknown_theory o
   16.12 +      Toplevel.keep (fn state => code_thms_cmd (Toplevel.theory_of state) cs)));
   16.13  
   16.14  val _ =
   16.15    Outer_Syntax.improper_command @{command_spec "code_deps"}
   16.16      "visualize dependencies of code equations for code"
   16.17 -    (Scan.repeat1 Parse.term_group
   16.18 -      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   16.19 -        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
   16.20 +    (Scan.repeat1 Parse.term_group >> (fn cs =>
   16.21 +      Toplevel.unknown_theory o
   16.22 +      Toplevel.keep (fn state => code_deps_cmd (Toplevel.theory_of state) cs)));
   16.23  
   16.24  end;
   16.25  
    17.1 --- a/src/Tools/induct.ML	Tue Apr 09 13:55:28 2013 +0200
    17.2 +++ b/src/Tools/induct.ML	Tue Apr 09 15:29:25 2013 +0200
    17.3 @@ -261,7 +261,7 @@
    17.4  val _ =
    17.5    Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
    17.6      "print induction and cases rules"
    17.7 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    17.8 +    (Scan.succeed (Toplevel.unknown_context o
    17.9        Toplevel.keep (print_rules o Toplevel.context_of)));
   17.10  
   17.11  
    18.1 --- a/src/Tools/quickcheck.ML	Tue Apr 09 13:55:28 2013 +0200
    18.2 +++ b/src/Tools/quickcheck.ML	Tue Apr 09 15:29:25 2013 +0200
    18.3 @@ -533,7 +533,7 @@
    18.4    Outer_Syntax.improper_command @{command_spec "quickcheck"}
    18.5      "try to find counterexample for subgoal"
    18.6      (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
    18.7 -      Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
    18.8 +      Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
    18.9  
   18.10  
   18.11  (* automatic testing *)
    19.1 --- a/src/Tools/value.ML	Tue Apr 09 13:55:28 2013 +0200
    19.2 +++ b/src/Tools/value.ML	Tue Apr 09 15:29:25 2013 +0200
    19.3 @@ -65,8 +65,7 @@
    19.4  val _ =
    19.5    Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
    19.6      (opt_evaluator -- opt_modes -- Parse.term
    19.7 -      >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
    19.8 -          (value_cmd some_name modes t)));
    19.9 +      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
   19.10  
   19.11  val antiq_setup =
   19.12    Thy_Output.antiquotation @{binding value}
    20.1 --- a/src/ZF/Tools/typechk.ML	Tue Apr 09 13:55:28 2013 +0200
    20.2 +++ b/src/ZF/Tools/typechk.ML	Tue Apr 09 15:29:25 2013 +0200
    20.3 @@ -122,7 +122,7 @@
    20.4  
    20.5  val _ =
    20.6    Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
    20.7 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    20.8 +    (Scan.succeed (Toplevel.unknown_context o
    20.9        Toplevel.keep (print_tcset o Toplevel.context_of)));
   20.10  
   20.11