global state transformation: non-critical, but also non-thread-safe;
authorwenzelm
Thu, 16 Aug 2007 18:53:21 +0200
changeset 24295 af8dbc7a2305
parent 24294 edfe16773fd4
child 24296 3479a9fe73e0
global state transformation: non-critical, but also non-thread-safe;
src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Aug 16 11:45:07 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 16 18:53:21 2007 +0200
@@ -715,17 +715,17 @@
 fun exn () = snd (! global_state);
 
 
-(* apply transformers to global state *)
+(* apply transformers to global state --- NOT THREAD-SAFE! *)
 
 nonfix >> >>>;
 
-fun >> tr = NAMED_CRITICAL "toplevel" (fn () =>
+fun >> tr =
   (case apply true tr (get_state ()) of
     NONE => false
   | SOME (state', exn_info) =>
       (global_state := (state', exn_info);
         print_exn exn_info;
-        true)));
+        true));
 
 fun >>> [] = ()
   | >>> (tr :: trs) = if >> tr then >>> trs else ();