# 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;