# HG changeset patch
# User wenzelm
# Date 1228428166 -3600
# Node ID 53c96f58e38f0bc686f0985e4a6a147c1fc5f18d
# Parent  ec120dc11e8b0096a1e2323f2b1b91b01377b74e
future_scheduler: no global task group, exceptions via collective join;
finish: removed PureThy.force_proofs, back to old version;

diff -r ec120dc11e8b -r 53c96f58e38f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Dec 04 23:01:11 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Dec 04 23:02:46 2008 +0100
@@ -320,14 +320,12 @@
     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 true body;
+        val x = Future.future NONE deps true body;
       in (x, Symtab.update (name, Future.task_of x) tab) end;
     val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
-    val _ = List.app (PureThy.force_proofs o get_theory o #1) tasks;
   in () end;
 
 local
@@ -589,8 +587,6 @@
 
 (* finish all theories *)
 
-fun finish () = change_thys (Graph.map_nodes
-  (fn (SOME _, SOME thy) => (NONE, (PureThy.force_proofs thy; SOME thy))
-    | (_, entry) => (NONE, entry)));
+fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
 
 end;