# HG changeset patch
# User wenzelm
# Date 1120221722 -7200
# Node ID f6173a9aee5a6a4eca84086e030f6d263383cdd0
# Parent  a6f65f47eda1246967ea0624575628d1bde9500a
added profile flag;

diff -r a6f65f47eda1 -r f6173a9aee5a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Jul 01 14:42:01 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Jul 01 14:42:02 2005 +0200
@@ -67,6 +67,7 @@
   val unknown_context: transition -> transition
   val quiet: bool ref
   val debug: bool ref
+  val profiling: int ref
   val exn_message: exn -> string
   val apply: bool -> transition -> state -> (state * (exn * string) option) option
   val excursion_result: ((transition * (state -> state -> 'a -> 'a)) list * 'a) -> 'a
@@ -421,6 +422,7 @@
 
 val quiet = ref false;
 val debug = ref false;
+val profiling = ref 0;
 
 
 (* print exceptions *)
@@ -498,7 +500,7 @@
       else warning (command_msg "Interactive-only " tr);
     val (result, opt_exn) =
       (if ! Output.timing andalso not no_timing then (info (command_msg "" tr); timeap) else I)
-        (apply_trans int trans) state;
+        (profile (! profiling) (apply_trans int trans)) state;
     val _ = conditional (int andalso not (! quiet) andalso
         exists (fn m => m mem_string print) ("" :: ! print_mode))
       (fn () => print_state false result);