# HG changeset patch # User wenzelm # Date 1185375950 -7200 # Node ID e3c4c0b9ae0544614fa8cfdcb0be6d30ba0e3dec # Parent 03b71bf913184277d8e082b24de9ccc0b97e3291 require_thy/schedule: improved task graph, actually observe dependencies on running tasks; diff -r 03b71bf91318 -r e3c4c0b9ae05 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Jul 25 17:05:49 2007 +0200 +++ b/src/Pure/Thy/thy_info.ML Wed Jul 25 17:05:50 2007 +0200 @@ -49,7 +49,6 @@ structure ThyInfo: THY_INFO = struct - (** theory loader actions and hooks **) datatype action = Update | Outdate | Remove; @@ -373,7 +372,7 @@ val _ = member (op =) initiators name andalso error (cycle_msg initiators); in (case try (Graph.get_node (fst tasks)) name of - SOME task => (is_none task, tasks) + SOME task => (Task.is_finished task, tasks) | NONE => let val (current, deps, parents) = check_deps ml strict dir' name @@ -391,8 +390,8 @@ val _ = change_thys (new_deps name parent_names (deps, thy)); val tasks_graph'' = tasks_graph' |> new_deps name parent_names - (if all_current then NONE - else SOME (fn () => load_thy really ml time initiators dir' name)); + (if all_current then Task.Finished + else Task.Task (fn () => load_thy really ml time initiators dir' name)); val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1; in (all_current, (tasks_graph'', tasks_len'')) end) end; @@ -400,20 +399,27 @@ end; -(* use_thy etc. -- scheduling required theories *) +(* variations on use_thy -- scheduling required theories *) local fun schedule_seq tasks = Graph.topological_order tasks - |> List.app (fn name => the_default I (Graph.get_node tasks name) ()); + |> List.app (fn name => (case Graph.get_node tasks name of Task.Task f => f () | _ => ())); -fun next_task (SOME f :: fs, G) = (SOME f, (fs, G)) - | next_task (NONE :: fs, G) = next_task (fs, G) - | next_task ([], G) = - (case Graph.minimals G of - [] => (NONE, ([], G)) - | ms => next_task (map (Graph.get_node G) ms, Graph.del_nodes ms G)); +fun next_task G = + let + val tasks = map (fn name => (name, Graph.get_node G name)) (Graph.minimals G); + val finished = filter (Task.is_finished o snd) tasks; + in + if not (null finished) then next_task (Graph.del_nodes (map fst finished) G) + else if null tasks then ((Task.Finished, I), G) + else + (case find_first (not o Task.is_running o snd) tasks of + NONE => ((Task.Running, I), G) + | SOME (name, task) => + ((task, Graph.del_nodes [name]), Graph.map_node name (K Task.Running) G)) + end; fun schedule_tasks (tasks, n) = let val m = ! Multithreading.max_threads in @@ -422,7 +428,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 Multithreading.schedule (Int.min (m, n)) next_task tasks of [] => () | exns => raise Exn.EXCEPTIONS (exns, "")) end;