# HG changeset patch # User wenzelm # Date 1231680154 -3600 # Node ID da9268ac78b75167dfba6bbdd80bd0ac015deb54 # Parent 7b09624f6bc1416b1f590e6ffc8bfac0c213f651# Parent a96236886804a65992cad318cfdbfa7f884e40de merged diff -r 7b09624f6bc1 -r da9268ac78b7 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Jan 11 14:18:32 2009 +0100 +++ b/src/Pure/Thy/thy_info.ML Sun Jan 11 14:22:34 2009 +0100 @@ -350,6 +350,8 @@ 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 par_proofs = ! parallel_proofs; + fun fork (name, body) tab = let val deps = Graph.imm_preds task_graph name @@ -357,12 +359,15 @@ (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE)); fun failed (parent, future) = if can Future.join future then NONE else SOME parent; - val x = Future.fork_deps (map #2 deps) (fn () => + val future = Future.fork_deps (map #2 deps) (fn () => (case map_filter failed deps of [] => body () | bad => error (loader_msg ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") []))); - in Symtab.update (name, x) tab end; + val future' = + if par_proofs then future + else Future.map (fn after_load => (after_load (); fn () => ())) future; + in Symtab.update (name, future') tab end; val futures = fold fork tasks Symtab.empty; diff -r 7b09624f6bc1 -r da9268ac78b7 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Jan 11 14:18:32 2009 +0100 +++ b/src/Pure/thm.ML Sun Jan 11 14:22:34 2009 +0100 @@ -1613,7 +1613,7 @@ val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val i = serial (); - val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof); + val future = future_thm |> Future.map (future_result i thy sorts prop); val promise = (i, future); in Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),