src/Pure/thm.ML
changeset 28429 3d5fbf964a7e
parent 28391 1a4804fc2216
child 28441 9b0daffc4054
     1.1 --- a/src/Pure/thm.ML	Tue Sep 30 14:30:44 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Sep 30 22:02:44 2008 +0200
     1.3 @@ -151,6 +151,7 @@
     1.4    val varifyT: thm -> thm
     1.5    val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
     1.6    val freezeT: thm -> thm
     1.7 +  val join_futures: theory -> unit
     1.8    val promise: (unit -> thm) -> cterm -> thm
     1.9    val proof_of: thm -> Proofterm.proof
    1.10    val extern_oracles: theory -> xstring list
    1.11 @@ -1606,18 +1607,13 @@
    1.12    fun merge _ _ : T = ref [];
    1.13  );
    1.14  
    1.15 +val _ = Context.>> (Context.map_theory Futures.init);
    1.16 +
    1.17  fun add_future thy future = CRITICAL (fn () => change (Futures.get thy) (cons future));
    1.18  
    1.19  fun join_futures thy =
    1.20 -  let
    1.21 -    val futures = Futures.get thy;
    1.22 -    val results = Future.join_results (rev (! futures));
    1.23 -    val done = CRITICAL (fn () =>
    1.24 -      (change futures (filter_out Future.is_finished); null (! futures)));
    1.25 -    val _ = Future.release_results results;
    1.26 -  in if done then NONE else SOME thy end;
    1.27 -
    1.28 -val _ = Context.>> (Context.map_theory (Futures.init #> Theory.at_end join_futures));
    1.29 +  (case CRITICAL (fn () => ! (Futures.get thy)) of [] => ()
    1.30 +  | futures => (Future.release_results (Future.join_results (rev futures)); join_futures thy));
    1.31  
    1.32  
    1.33  (* promise *)
    1.34 @@ -1644,7 +1640,7 @@
    1.35      val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]);
    1.36  
    1.37      val i = serial ();
    1.38 -    val future = Future.fork_irrelevant (promise_result i thy sorts prop o make_result);
    1.39 +    val future = Future.fork_background (promise_result i thy sorts prop o make_result);
    1.40      val _ = add_future thy future;
    1.41    in
    1.42      Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop),