# HG changeset patch
# User wenzelm
# Date 1220802399 -7200
# Node ID a472d844994e4dfd3cabde9f51aa938929aee6c7
# Parent  b44a7b2599095e23dbe042959a6b74a494ad2c68
tuned;

diff -r b44a7b259909 -r a472d844994e src/Pure/Concurrent/schedule.ML
--- a/src/Pure/Concurrent/schedule.ML	Sun Sep 07 17:46:38 2008 +0200
+++ b/src/Pure/Concurrent/schedule.ML	Sun Sep 07 17:46:39 2008 +0200
@@ -20,9 +20,9 @@
 
 fun schedule n next_task = uninterruptible (fn restore_attributes => fn tasks =>
   let
-    (*protected execution*)
+    (*synchronized execution*)
     val lock = Mutex.mutex ();
-    fun PROTECTED e =
+    fun SYNCHRONIZED e =
       let
         val _ = Mutex.lock lock;
         val res = Exn.capture e ();
@@ -66,20 +66,20 @@
 
     (*worker thread*)
     fun worker () =
-      (case PROTECTED dequeue of
+      (case SYNCHRONIZED dequeue of
         Task {body, cont, fail} =>
           (case Exn.capture (restore_attributes body) () of
             Exn.Result () =>
-              (PROTECTED (fn () => (change queue cont; wakeup_all ())); worker ())
+              (SYNCHRONIZED (fn () => (change queue cont; wakeup_all ())); worker ())
           | Exn.Exn exn =>
-              PROTECTED (fn () =>
+              SYNCHRONIZED (fn () =>
                 (change status (cons exn); change queue fail; stop (); wakeup_all ())))
-      | Terminate => PROTECTED (fn () => (stop (); wakeup_all ())));
+      | Terminate => SYNCHRONIZED (fn () => (stop (); wakeup_all ())));
 
     (*main control: fork and wait*)
     fun fork 0 = ()
       | fork k = (start worker; fork (k - 1));
-    val _ = PROTECTED (fn () =>
+    val _ = SYNCHRONIZED (fn () =>
      (fork (Int.max (n, 1));
       while not (null (! running)) do
       (trace_active ();