# HG changeset patch
# User wenzelm
# Date 1221076232 -7200
# Node ID c6dad24124f141ab4651e5f28d02b0a207f70c6f
# Parent  7ed74d0ba6077b1a461f79fc91f34cc083db6537
added future_scheduler (default false);

diff -r 7ed74d0ba607 -r c6dad24124f1 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Sep 10 21:50:30 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Sep 10 21:50:32 2008 +0200
@@ -29,6 +29,7 @@
   val exec_file: bool -> Path.T -> Context.generic -> Context.generic
   val use: string -> unit
   val time_use: string -> unit
+  val future_scheduler: bool ref
   val use_thys: string list -> unit
   val use_thy: string -> unit
   val time_use_thy: string -> unit
@@ -315,6 +316,28 @@
 datatype task = Task of (unit -> unit) | Finished | Running;
 fun task_finished Finished = true | task_finished _ = false;
 
+val future_scheduler = ref false;
+
+fun future_schedule task_graph =
+  let
+    val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
+      (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
+
+    val group = TaskQueue.new_group ();
+    fun future (name, body) tab =
+      let
+        val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
+        val x = Future.future (SOME group) deps body;
+      in (x, Symtab.update (name, Future.task_of x) tab) end;
+
+    val exns = #1 (fold_map future tasks Symtab.empty)
+      |> Future.join_results
+      |> map_filter Exn.get_exn;
+  in
+    if null exns then ()
+    else raise Exn.EXCEPTIONS (exns, "")
+  end;
+
 local
 
 fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m))
@@ -351,6 +374,7 @@
     else if Multithreading.self_critical () then
      (warning (loader_msg "no multithreading within critical section" []);
       schedule_seq tasks)
+    else if ! future_scheduler then future_schedule tasks
     else
       (case Schedule.schedule (Int.min (m, n)) next_task tasks of
         [] => ()
@@ -578,4 +602,3 @@
 fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
 
 end;
-