# HG changeset patch
# User wenzelm
# Date 1228428058 -3600
# Node ID c549650d1442a788e4238f871a627da0e9b7d00f
# Parent  cb8a2c3e188f6be525e090215ba788b8b38ff187
future proofs: pass actual futures to facilitate composite computations;

diff -r cb8a2c3e188f -r c549650d1442 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Dec 04 23:00:27 2008 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Dec 04 23:00:58 2008 +0100
@@ -115,7 +115,7 @@
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   val is_relevant: state -> bool
-  val future_proof: (state -> context) -> state -> context
+  val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
 end;
 
 structure Proof: PROOF =
@@ -990,7 +990,7 @@
   not (is_initial state) orelse
   schematic_goal state;
 
-fun future_proof make_proof state =
+fun future_proof proof state =
   let
     val _ = is_relevant state andalso error "Cannot fork relevant proof";
 
@@ -1004,16 +1004,19 @@
     fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
     val this_name = ProofContext.full_name (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
 
-    fun make_result () = state
+    val result_ctxt =
+      state
       |> map_contexts (Variable.auto_fixes prop)
       |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
-      |> make_proof
-      |> (fn result_ctxt => ProofContext.get_fact_single result_ctxt (Facts.named this_name));
-    val finished_goal = Goal.protect (Goal.future_result goal_ctxt make_result prop);
-  in
-    state
-    |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
-    |> global_done_proof
-  end;
+      |> proof;
+
+    val thm = result_ctxt |> Future.map (fn (_, ctxt) =>
+      ProofContext.get_fact_single ctxt (Facts.named this_name));
+    val finished_goal = Goal.protect (Goal.future_result goal_ctxt thm prop);
+    val state' =
+      state
+      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
+      |> global_done_proof;
+  in (Future.map #1 result_ctxt, state') end;
 
 end;
diff -r cb8a2c3e188f -r c549650d1442 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Dec 04 23:00:27 2008 +0100
+++ b/src/Pure/goal.ML	Thu Dec 04 23:00:58 2008 +0100
@@ -20,7 +20,7 @@
   val conclude: thm -> thm
   val finish: thm -> thm
   val norm_result: thm -> thm
-  val future_result: Proof.context -> (unit -> thm) -> term -> thm
+  val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
@@ -116,11 +116,11 @@
 
     val global_prop =
       Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
-    val global_result =
-      Thm.generalize (map #1 tfrees, []) 0 o
-      Drule.forall_intr_list fixes o
-      Drule.implies_intr_list assms o
-      Thm.adjust_maxidx_thm ~1 o result;
+    val global_result = result |> Future.map
+      (Thm.adjust_maxidx_thm ~1 #>
+        Drule.implies_intr_list assms #>
+        Drule.forall_intr_list fixes #>
+        Thm.generalize (map #1 tfrees, []) 0);
     val local_result =
       Thm.future global_result (cert global_prop)
       |> Thm.instantiate (instT, [])
@@ -178,7 +178,7 @@
           end);
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
-      else future_result ctxt' result (Thm.term_of stmt);
+      else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)