Toplevel.no_timing;

--- a/src/Provers/classical.ML	Wed May 31 14:29:29 2000 +0200
+++ b/src/Provers/classical.ML	Wed May 31 14:29:42 2000 +0200
@@ -1188,8 +1188,8 @@
 val print_clasetP =
   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
     OuterSyntax.Keyword.diag
-    (Scan.succeed (Toplevel.keep
-      (Toplevel.node_case print_claset (print_local_claset o Proof.context_of))));
+    (Scan.succeed (Toplevel.no_timing o (Toplevel.keep
+      (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))));
 
 val _ = OuterSyntax.add_parsers [print_clasetP];
 

--- a/src/Provers/simplifier.ML	Wed May 31 14:29:29 2000 +0200
+++ b/src/Provers/simplifier.ML	Wed May 31 14:29:42 2000 +0200
@@ -551,8 +551,8 @@
 val print_simpsetP =
   OuterSyntax.improper_command "print_simpset" "print context of Simplifier"
     OuterSyntax.Keyword.diag
-    (Scan.succeed (Toplevel.keep
-      (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of))));
+    (Scan.succeed (Toplevel.no_timing o (Toplevel.keep
+      (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of)))));
 
 val _ = OuterSyntax.add_parsers [print_simpsetP];
 

--- a/src/Pure/Interface/proof_general.ML	Wed May 31 14:29:29 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Wed May 31 14:29:42 2000 +0200
@@ -208,35 +208,38 @@
 
 val old_undoP =	(* FIXME same name for compatibility with PG/Isabelle99 *)
   OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
-    (Scan.succeed IsarCmd.undo);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
 
 val undoP =
   OuterSyntax.improper_command "ProofGeneral.undo" "undo last command (no output)" K.control
-    (Scan.succeed IsarCmd.undo);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
 
 val context_thy_onlyP =
   OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
-    (P.name >> IsarThy.init_context update_thy_only);
+    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
 
 val try_context_thy_onlyP =
   OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
-    (P.name >> (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only));
+    (P.name >> (Toplevel.no_timing oo
+      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
 
 val restartP =
   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
-    (P.opt_unit >> K (Toplevel.imperative isar_restart));
+    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
 
 val kill_proofP =
   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
-    (Scan.succeed (IsarCmd.kill_proof_notify tell_clear_goals));
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
 
 val inform_file_processedP =
   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
-    (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_processed name)));
+    (P.name >> (Toplevel.no_timing oo
+      (fn name => Toplevel.imperative (fn () => inform_file_processed name))));
 
 val inform_file_retractedP =
   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
-    (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name)));
+    (P.name >> (Toplevel.no_timing oo
+      (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
 
 fun init_outer_syntax () = OuterSyntax.add_parsers
  [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,

--- a/src/Pure/Isar/isar_syn.ML	Wed May 31 14:29:29 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed May 31 14:29:42 2000 +0200
@@ -208,7 +208,7 @@
 
 val useP =
   OuterSyntax.command "use" "eval ML text from file" K.diag
-    (P.name >> IsarCmd.use);
+    (P.name >> (Toplevel.no_timing oo IsarCmd.use));
 
 val mlP =
   OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
@@ -451,27 +451,27 @@
 
 val cannot_undoP =
   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
-    (P.name >> IsarCmd.cannot_undo);
+    (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
 
 val clear_undosP =
   OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
-    (P.nat >> IsarCmd.clear_undos_theory);
+    (P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory));
 
 val redoP =
   OuterSyntax.improper_command "redo" "redo last command" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.redo));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
 
 val undos_proofP =
   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
-    (P.nat >> (Toplevel.print oo IsarCmd.undos_proof));
+    (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof));
 
 val undoP =
   OuterSyntax.improper_command "undo" "undo last command" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.undo));
+    (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo));
 
 val killP =
   OuterSyntax.improper_command "kill" "kill current history node" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.kill));
+    (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill));
 
 
 
@@ -482,67 +482,67 @@
 
 val pretty_setmarginP =
   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
-    K.diag (P.nat >> IsarCmd.pretty_setmargin);
+    K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
 
 val print_commandsP =
   OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
-    (Scan.succeed OuterSyntax.print_help);
+    (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_help));
 
 val print_contextP =
   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
-    (Scan.succeed IsarCmd.print_context);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
 
 val print_theoryP =
   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
-    (Scan.succeed IsarCmd.print_theory);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theory));
 
 val print_syntaxP =
   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
-    (Scan.succeed IsarCmd.print_syntax);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
 
 val print_theoremsP =
   OuterSyntax.improper_command "print_theorems" "print theorems known in this theory" K.diag
-    (Scan.succeed IsarCmd.print_theorems);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
 
 val print_attributesP =
   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
-    (Scan.succeed IsarCmd.print_attributes);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
 
 val print_methodsP =
   OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag
-    (Scan.succeed IsarCmd.print_methods);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
 
 val thms_containingP =
   OuterSyntax.improper_command "thms_containing" "print theorems containing all given constants"
-    K.diag (Scan.repeat P.xname >> IsarCmd.print_thms_containing);
+    K.diag (Scan.repeat P.xname >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
 
 val print_bindsP =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
-    (Scan.succeed IsarCmd.print_binds);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
 
 val print_lthmsP =
   OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
-    (Scan.succeed IsarCmd.print_lthms);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_lthms));
 
 val print_casesP =
   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
-    (Scan.succeed IsarCmd.print_cases);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
 
 val print_thmsP =
   OuterSyntax.improper_command "thm" "print theorems" K.diag
-    (opt_modes -- P.xthms1 >> IsarCmd.print_thms);
+    (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
 
 val print_propP =
   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
-    (opt_modes -- P.term >> IsarCmd.print_prop);
+    (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
 
 val print_termP =
   OuterSyntax.improper_command "term" "read and print term" K.diag
-    (opt_modes -- P.term >> IsarCmd.print_term);
+    (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
 
 val print_typeP =
   OuterSyntax.improper_command "typ" "read and print type" K.diag
-    (opt_modes -- P.typ >> IsarCmd.print_type);
+    (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
 
 
 
@@ -550,79 +550,79 @@
 
 val cdP =
   OuterSyntax.improper_command "cd" "change current working directory" K.diag
-    (P.name >> IsarCmd.cd);
+    (P.name >> (Toplevel.no_timing oo IsarCmd.cd));
 
 val pwdP =
   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
-    (Scan.succeed IsarCmd.pwd);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
 
 val use_thyP =
   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
-    (P.name >> IsarCmd.use_thy);
+    (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
 
 val use_thy_onlyP =
   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
-    K.diag (P.name >> IsarCmd.use_thy_only);
+    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only));
 
 val update_thyP =
   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
-    (P.name >> IsarCmd.update_thy);
+    (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
 
 val update_thy_onlyP =
   OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML"
-    K.diag (P.name >> IsarCmd.update_thy_only);
+    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only));
 
 val touch_thyP =
   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
-    (P.name >> IsarCmd.touch_thy);
+    (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
 
 val touch_all_thysP =
   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
-    (Scan.succeed IsarCmd.touch_all_thys);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
 
 val touch_child_thysP =
   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
-    (P.name >> IsarCmd.touch_child_thys);
+    (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
 
 val remove_thyP =
   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
-    (P.name >> IsarCmd.remove_thy);
+    (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
 
 val kill_thyP =
   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
-    K.diag (P.name >> IsarCmd.kill_thy);
+    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
 
 val prP =
   OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
-    (opt_modes -- Scan.option P.nat >> IsarCmd.pr);
+    (opt_modes -- Scan.option P.nat >> (Toplevel.no_timing oo IsarCmd.pr));
 
 val disable_prP =
   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
-    (Scan.succeed IsarCmd.disable_pr);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
 
 val enable_prP =
   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
-    (Scan.succeed IsarCmd.enable_pr);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
 
 val commitP =
   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
-    (P.opt_unit >> (K IsarCmd.use_commit));
+    (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
 
 val quitP =
   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
-    (P.opt_unit >> (K IsarCmd.quit));
+    (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
 
 val exitP =
   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
-    (Scan.succeed IsarCmd.exit);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
 
 val init_toplevelP =
   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
-    (Scan.succeed IsarCmd.init_toplevel);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel));
 
 val welcomeP =
   OuterSyntax.improper_command "welcome" "print welcome message" K.diag
-    (Scan.succeed IsarCmd.welcome);
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
 
 
 

--- a/src/Pure/Isar/toplevel.ML	Wed May 31 14:29:29 2000 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 31 14:29:42 2000 +0200
@@ -35,6 +35,7 @@
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
   val print: transition -> transition
+  val no_timing: transition -> transition
   val reset: transition -> transition
   val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
   val exit: transition -> transition
@@ -272,15 +273,17 @@
   pos: Position.T,
   int_only: bool,
   print: bool,
+  no_timing: bool,
   trans: trans list};
 
-fun make_transition (name, pos, int_only, print, trans) =
-  Transition {name = name, pos = pos, int_only = int_only, print = print, trans = trans};
+fun make_transition (name, pos, int_only, print, no_timing, trans) =
+  Transition {name = name, pos = pos, int_only = int_only, print = print,
+    no_timing = no_timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, int_only, print, trans}) =
-  make_transition (f (name, pos, int_only, print, trans));
+fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) =
+  make_transition (f (name, pos, int_only, print, no_timing, trans));
 
-val empty = make_transition ("<unknown>", Position.none, false, false, []);
+val empty = make_transition ("<unknown>", Position.none, false, false, false, []);
 
 
 (* diagnostics *)
@@ -296,20 +299,23 @@
 
 (* modify transitions *)
 
-fun name nm = map_transition
-  (fn (_, pos, int_only, print, trans) => (nm, pos, int_only, print, trans));
+fun name nm = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
+  (nm, pos, int_only, print, no_timing, trans));
 
-fun position pos = map_transition
-  (fn (name, _, int_only, print, trans) => (name, pos, int_only, print, trans));
+fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) =>
+  (name, pos, int_only, print, no_timing, trans));
+
+fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) =>
+  (name, pos, int_only, print, no_timing, trans));
 
-fun interactive int_only = map_transition
-  (fn (name, pos, _, print, trans) => (name, pos, int_only, print, trans));
+val print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
+  (name, pos, int_only, true, no_timing, trans));
 
-val print = map_transition
-  (fn (name, pos, int_only, _, trans) => (name, pos, int_only, true, trans));
+val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
+  (name, pos, int_only, print, true, trans));
 
-fun add_trans tr = map_transition
-  (fn (name, pos, int_only, print, trans) => (name, pos, int_only, print, trans @ [tr]));
+fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) =>
+  (name, pos, int_only, print, no_timing, trans @ [tr]));
 
 
 (* build transitions *)
@@ -381,13 +387,14 @@
 
 local
 
-fun app int (tr as Transition {trans, int_only, print, ...}) state =
+fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
   let
     val _ =
       if int orelse not int_only then ()
       else warning (command_msg "Interactive-only " tr);
     val (result, opt_exn) =
-      (if ! Library.timing then (warning (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
+      (if ! Library.timing andalso not no_timing then (warning (command_msg "" tr); timeap) else I)
+        (apply_trans int trans) state;
     val _ = if int andalso print andalso not (! quiet) then print_state false result else ();
   in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;