# HG changeset patch # User wenzelm # Date 1190407873 -7200 # Node ID f311717d1f03470efe8956f246e6a80d362c4817 # Parent 35075a1e9599205c6c22a6e5b270af403406a60a tuned; diff -r 35075a1e9599 -r f311717d1f03 src/Pure/ML-Systems/multithreading_polyml.ML --- 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;