discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
authorwenzelm
Mon, 21 Dec 2015 14:18:57 +0100
changeset 61884 d4c89ea5e6dc
parent 61883 c0f34fe6aa61
child 61885 acdfc76a6c33
discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Dec 21 13:39:45 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Dec 21 14:18:57 2015 +0100
@@ -26,7 +26,6 @@
   val pretty_state: state -> Pretty.T list
   val string_of_state: state -> string
   val pretty_abstract: state -> Pretty.T
-  val profiling: int Unsynchronized.ref
   type transition
   val empty: transition
   val name_of: transition -> string
@@ -204,9 +203,6 @@
 
 (** toplevel transitions **)
 
-val profiling = Unsynchronized.ref 0;
-
-
 (* node transactions -- maintaining stable checkpoints *)
 
 exception FAILURE of state * exn;
@@ -568,10 +564,7 @@
   setmp_thread_position tr (fn state =>
     let
       val timing_start = Timing.start ();
-
-      val (result, opt_err) =
-         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
-
+      val (result, opt_err) = apply_trans int trans state;
       val timing_result = Timing.result timing_start;
       val timing_props =
         Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);