general Graph.schedule;

--- a/src/Pure/General/graph.ML	Fri Aug 12 15:30:12 2011 +0200
+++ b/src/Pure/General/graph.ML	Fri Aug 12 20:32:25 2011 +0200
@@ -49,6 +49,8 @@
   val topological_order: 'a T -> key list
   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
+  exception DEP of key * key
+  val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
 end;
 
 functor Graph(Key: KEY): GRAPH =
@@ -285,6 +287,24 @@
     |> fold add_edge_trans_acyclic (diff_edges G2 G1);
 
 
+(* schedule acyclic graph *)
+
+exception DEP of key * key;
+
+fun schedule f G =
+  let
+    val xs = topological_order G;
+    val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
+      let
+        val a = get_node G x;
+        val deps = imm_preds G x |> map (fn y =>
+          (case Table.lookup tab y of
+            SOME b => (y, b)
+          | NONE => raise DEP (x, y)));
+      in Table.update (x, f deps (x, a)) tab end);
+  in map (the o Table.lookup results) xs end;
+
+
 (*final declarations of this structure!*)
 val map = map_nodes;
 val fold = fold_graph;

--- a/src/Pure/Thy/thy_info.ML	Fri Aug 12 15:30:12 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Aug 12 20:32:25 2011 +0200
@@ -178,51 +178,37 @@
 fun task_finished (Task _) = false
   | task_finished (Finished _) = true;
 
+fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
+
 local
 
 fun finish_thy ((thy, present, commit): result) =
   (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
 
-fun schedule_seq task_graph =
-  ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
-    (case Graph.get_node task_graph name of
-      Task (parents, body) =>
-        let val result = body (map (the o Symtab.lookup tab) parents)
-        in Symtab.update (name, finish_thy result) tab end
-    | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
-
-fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
-  let
-    val tasks = Graph.topological_order task_graph;
-    val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
-      (case Graph.get_node task_graph name of
-        Task (parents, body) =>
-          let
-            val get = the o Symtab.lookup tab;
-            val deps = map (`get) (Graph.imm_preds task_graph name);
-            val task_deps = map (Future.task_of o #1) deps;
-            fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
+val schedule_seq =
+  Graph.schedule (fn deps => fn (_, task) =>
+    (case task of
+      Task (parents, body) => finish_thy (body (task_parents deps parents))
+    | Finished thy => thy)) #> ignore;
 
-            val future =
-              singleton
-                (Future.forks
-                  {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0,
-                    interrupts = true})
-                (fn () =>
-                  (case map_filter failed deps of
-                    [] => body (map (#1 o Future.join o get) parents)
-                  | bad => error (loader_msg ("failed to load " ^ quote name ^
-                      " (unresolved " ^ commas_quote bad ^ ")") [])));
-          in Symtab.update (name, future) tab end
-      | Finished thy => Symtab.update (name, Future.value (thy, Future.value (), I)) tab));
-    val _ =
-      tasks |> maps (fn name =>
-        let
-          val result = Future.join (the (Symtab.lookup futures name));
-          val _ = finish_thy result;
-        in [] end handle exn => [Exn.Exn exn])
-      |> rev |> Exn.release_all;
-  in () end) ();
+val schedule_futures = uninterruptible (fn _ =>
+  Graph.schedule (fn deps => fn (name, task) =>
+    (case task of
+      Task (parents, body) =>
+        singleton
+          (Future.forks
+            {name = "theory:" ^ name, group = NONE,
+              deps = map (Future.task_of o #2) deps,
+              pri = 0, interrupts = true})
+          (fn () =>
+            (case filter (not o can Future.join o #2) deps of
+              [] => body (map (#1 o Future.join) (task_parents deps parents))
+            | bad =>
+                error (loader_msg ("failed to load " ^ quote name ^
+                  " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
+    | Finished thy => Future.value (thy, Future.value (), I)))
+  #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
+  #> rev #> Exn.release_all) #> ignore;
 
 in