1.1 --- a/src/Pure/Thy/thy_info.ML	Sat Jul 02 19:08:51 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Jul 02 19:22:06 2011 +0200
     1.3 @@ -165,8 +165,10 @@
     1.4  
     1.5  (* scheduling loader tasks *)
     1.6  
     1.7 +type result = theory * unit future * (unit -> unit);
     1.8 +
     1.9  datatype task =
    1.10 -  Task of string list * (theory list -> (theory * unit future * (unit -> unit))) |
    1.11 +  Task of string list * (theory list -> result) |
    1.12    Finished of theory;
    1.13  
    1.14  fun task_finished (Task _) = false
    1.15 @@ -174,15 +176,15 @@
    1.16  
    1.17  local
    1.18  
    1.19 +fun finish_thy ((thy, present, commit): result) =
    1.20 +  (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
    1.21 +
    1.22  fun schedule_seq task_graph =
    1.23    ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
    1.24      (case Graph.get_node task_graph name of
    1.25        Task (parents, body) =>
    1.26 -        let
    1.27 -          val (thy, present, commit) = body (map (the o Symtab.lookup tab) parents);
    1.28 -          val _ = Future.join present;
    1.29 -          val _ = commit ();
    1.30 -        in Symtab.update (name, thy) tab end
    1.31 +        let val result = body (map (the o Symtab.lookup tab) parents)
    1.32 +        in Symtab.update (name, finish_thy result) tab end
    1.33      | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
    1.34  
    1.35  fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
    1.36 @@ -210,10 +212,8 @@
    1.37      val _ =
    1.38        tasks |> maps (fn name =>
    1.39          let
    1.40 -          val (thy, present, commit) = Future.join (the (Symtab.lookup futures name));
    1.41 -          val _ = Global_Theory.join_proofs thy;
    1.42 -          val _ = Future.join present;
    1.43 -          val _ = commit ();
    1.44 +          val result = Future.join (the (Symtab.lookup futures name));
    1.45 +          val _ = finish_thy result;
    1.46          in [] end handle exn => [Exn.Exn exn])
    1.47        |> rev |> Exn.release_all;
    1.48    in () end) ();