# HG changeset patch
# User wenzelm
# Date 1220537029 -7200
# Node ID 7332b623b569d361067c34656200e16cd84b9542
# Parent  e99427bcf7f3abb0ba6c7491480cb49cda840df9
moved Multithreading.task/schedule to Concurrent/schedule.ML

diff -r e99427bcf7f3 -r 7332b623b569 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Sep 04 16:03:48 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Sep 04 16:03:49 2008 +0200
@@ -329,12 +329,12 @@
     val finished = filter (task_finished o fst o snd) tasks;
   in
     if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
-    else if null tasks then (Multithreading.Terminate, G)
+    else if null tasks then (Schedule.Terminate, G)
     else
       (case fold max_task tasks NONE of
-        NONE => (Multithreading.Wait, G)
+        NONE => (Schedule.Wait, G)
       | SOME (name, (body, _)) =>
-         (Multithreading.Task {body = PrintMode.closure body,
+         (Schedule.Task {body = PrintMode.closure body,
            cont = Graph.del_nodes [name], fail = K Graph.empty},
           Graph.map_node name (K Running) G))
   end;
@@ -352,7 +352,7 @@
      (warning (loader_msg "no multithreading within critical section" []);
       schedule_seq tasks)
     else
-      (case Multithreading.schedule (Int.min (m, n)) next_task tasks of
+      (case Schedule.schedule (Int.min (m, n)) next_task tasks of
         [] => ()
       | exns => raise Exn.EXCEPTIONS (exns, ""))
   end;