--- a/src/Pure/ML-Systems/multithreading_polyml.ML Fri Sep 21 22:51:12 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Fri Sep 21 22:51:13 2007 +0200
@@ -133,16 +133,11 @@
datatype 'a task =
Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
-local
-
-val protected_name = ref "";
-
-in
-
fun schedule n next_task = uninterruptible (fn _ => fn tasks =>
let
(*protected execution*)
val lock = Mutex.mutex ();
+ val protected_name = ref "";
fun PROTECTED name e =
let
val name' = ! protected_name;
@@ -219,8 +214,6 @@
end;
-end;
-
val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
val CRITICAL = Multithreading.CRITICAL;
val ignore_interrupt = Multithreading.ignore_interrupt;