merged
authorwenzelm
Fri Dec 05 00:23:37 2008 +0100 (2008-12-05)
changeset 28981c9cf71e161b9
parent 28970 1c743f58781a
parent 28980 9d7ea903e877
child 28983 f88fbb0c4f17
merged
src/Pure/Isar/proof.ML
src/Pure/pure_thy.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Import/lazy_seq.ML	Thu Dec 04 09:12:41 2008 -0800
     1.2 +++ b/src/HOL/Import/lazy_seq.ML	Fri Dec 05 00:23:37 2008 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4  structure LazySeq :> LAZY_SEQ =
     1.5  struct
     1.6  
     1.7 -datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
     1.8 +datatype 'a seq = Seq of ('a * 'a seq) option lazy
     1.9  
    1.10  exception Empty
    1.11  
     2.1 --- a/src/Pure/Concurrent/future.ML	Thu Dec 04 09:12:41 2008 -0800
     2.2 +++ b/src/Pure/Concurrent/future.ML	Fri Dec 05 00:23:37 2008 +0100
     2.3 @@ -30,21 +30,23 @@
     2.4    val enabled: unit -> bool
     2.5    type task = TaskQueue.task
     2.6    type group = TaskQueue.group
     2.7 -  val thread_data: unit -> (string * task * group) option
     2.8 -  type 'a T
     2.9 -  val task_of: 'a T -> task
    2.10 -  val group_of: 'a T -> group
    2.11 -  val peek: 'a T -> 'a Exn.result option
    2.12 -  val is_finished: 'a T -> bool
    2.13 -  val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
    2.14 -  val fork: (unit -> 'a) -> 'a T
    2.15 -  val fork_background: (unit -> 'a) -> 'a T
    2.16 -  val join_results: 'a T list -> 'a Exn.result list
    2.17 -  val join_result: 'a T -> 'a Exn.result
    2.18 -  val join: 'a T -> 'a
    2.19 +  val thread_data: unit -> (string * task) option
    2.20 +  type 'a future
    2.21 +  val task_of: 'a future -> task
    2.22 +  val group_of: 'a future -> group
    2.23 +  val peek: 'a future -> 'a Exn.result option
    2.24 +  val is_finished: 'a future -> bool
    2.25 +  val fork: (unit -> 'a) -> 'a future
    2.26 +  val fork_group: group -> (unit -> 'a) -> 'a future
    2.27 +  val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
    2.28 +  val fork_background: (unit -> 'a) -> 'a future
    2.29 +  val join_results: 'a future list -> 'a Exn.result list
    2.30 +  val join_result: 'a future -> 'a Exn.result
    2.31 +  val join: 'a future -> 'a
    2.32 +  val map: ('a -> 'b) -> 'a future -> 'b future
    2.33    val focus: task list -> unit
    2.34    val interrupt_task: string -> unit
    2.35 -  val cancel: 'a T -> unit
    2.36 +  val cancel: 'a future -> unit
    2.37    val shutdown: unit -> unit
    2.38  end;
    2.39  
    2.40 @@ -63,7 +65,7 @@
    2.41  type task = TaskQueue.task;
    2.42  type group = TaskQueue.group;
    2.43  
    2.44 -local val tag = Universal.tag () : (string * task * group) option Universal.tag in
    2.45 +local val tag = Universal.tag () : (string * task) option Universal.tag in
    2.46    fun thread_data () = the_default NONE (Thread.getLocal tag);
    2.47    fun setmp_thread_data data f x = Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
    2.48  end;
    2.49 @@ -71,7 +73,7 @@
    2.50  
    2.51  (* datatype future *)
    2.52  
    2.53 -datatype 'a T = Future of
    2.54 +datatype 'a future = Future of
    2.55   {task: task,
    2.56    group: group,
    2.57    result: 'a Exn.result option ref};
    2.58 @@ -140,7 +142,7 @@
    2.59  fun execute name (task, group, run) =
    2.60    let
    2.61      val _ = trace_active ();
    2.62 -    val ok = setmp_thread_data (name, task, group) run ();
    2.63 +    val ok = setmp_thread_data (name, task) run ();
    2.64      val _ = SYNCHRONIZED "execute" (fn () =>
    2.65       (change queue (TaskQueue.finish task);
    2.66        if ok then ()
    2.67 @@ -246,10 +248,10 @@
    2.68        change_result queue (TaskQueue.enqueue group deps pri run) before notify_all ());
    2.69    in Future {task = task, group = group, result = result} end;
    2.70  
    2.71 -fun fork_common pri = future (Option.map #3 (thread_data ())) [] pri;
    2.72 -
    2.73 -fun fork e = fork_common true e;
    2.74 -fun fork_background e = fork_common false e;
    2.75 +fun fork e = future NONE [] true e;
    2.76 +fun fork_group group e = future (SOME group) [] true e;
    2.77 +fun fork_deps deps e = future NONE (map task_of deps) true e;
    2.78 +fun fork_background e = future NONE [] false e;
    2.79  
    2.80  
    2.81  (* join: retrieve results *)
    2.82 @@ -274,7 +276,7 @@
    2.83                (*alien thread -- refrain from contending for resources*)
    2.84                while exists (not o is_finished) xs
    2.85                do SYNCHRONIZED "join_thread" (fn () => wait "join_thread")
    2.86 -          | SOME (name, task, _) =>
    2.87 +          | SOME (name, task) =>
    2.88                (*proper task -- actively work towards results*)
    2.89                let
    2.90                  val unfinished = xs |> map_filter
    2.91 @@ -292,6 +294,8 @@
    2.92  fun join_result x = singleton join_results x;
    2.93  fun join x = Exn.release (join_result x);
    2.94  
    2.95 +fun map f x = fork_deps [x] (fn () => f (join x));
    2.96 +
    2.97  
    2.98  (* misc operations *)
    2.99  
   2.100 @@ -324,3 +328,6 @@
   2.101    else ();
   2.102  
   2.103  end;
   2.104 +
   2.105 +type 'a future = 'a Future.future;
   2.106 +
     3.1 --- a/src/Pure/Concurrent/par_list.ML	Thu Dec 04 09:12:41 2008 -0800
     3.2 +++ b/src/Pure/Concurrent/par_list.ML	Fri Dec 05 00:23:37 2008 +0100
     3.3 @@ -31,7 +31,7 @@
     3.4    if Future.enabled () then
     3.5      let
     3.6        val group = TaskQueue.new_group ();
     3.7 -      val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
     3.8 +      val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
     3.9        val _ = List.app (ignore o Future.join_result) futures;
    3.10      in Future.join_results futures end
    3.11    else map (Exn.capture f) xs;
     4.1 --- a/src/Pure/General/lazy.ML	Thu Dec 04 09:12:41 2008 -0800
     4.2 +++ b/src/Pure/General/lazy.ML	Fri Dec 05 00:23:37 2008 +0100
     4.3 @@ -8,13 +8,13 @@
     4.4  
     4.5  signature LAZY =
     4.6  sig
     4.7 -  type 'a T
     4.8 -  val same: 'a T * 'a T -> bool
     4.9 -  val lazy: (unit -> 'a) -> 'a T
    4.10 -  val value: 'a -> 'a T
    4.11 -  val peek: 'a T -> 'a Exn.result option
    4.12 -  val force: 'a T -> 'a
    4.13 -  val map_force: ('a -> 'a) -> 'a T -> 'a T
    4.14 +  type 'a lazy
    4.15 +  val same: 'a lazy * 'a lazy -> bool
    4.16 +  val lazy: (unit -> 'a) -> 'a lazy
    4.17 +  val value: 'a -> 'a lazy
    4.18 +  val peek: 'a lazy -> 'a Exn.result option
    4.19 +  val force: 'a lazy -> 'a
    4.20 +  val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
    4.21  end
    4.22  
    4.23  structure Lazy :> LAZY =
    4.24 @@ -22,13 +22,13 @@
    4.25  
    4.26  (* datatype *)
    4.27  
    4.28 -datatype 'a lazy =
    4.29 +datatype 'a T =
    4.30    Lazy of unit -> 'a |
    4.31    Result of 'a Exn.result;
    4.32  
    4.33 -type 'a T = 'a lazy ref;
    4.34 +type 'a lazy = 'a T ref;
    4.35  
    4.36 -fun same (r1: 'a T, r2) = r1 = r2;
    4.37 +fun same (r1: 'a lazy, r2) = r1 = r2;
    4.38  
    4.39  fun lazy e = ref (Lazy e);
    4.40  fun value x = ref (Result (Exn.Result x));
    4.41 @@ -58,3 +58,6 @@
    4.42  fun map_force f = value o f o force;
    4.43  
    4.44  end;
    4.45 +
    4.46 +type 'a lazy = 'a Lazy.lazy;
    4.47 +
     5.1 --- a/src/Pure/Isar/code.ML	Thu Dec 04 09:12:41 2008 -0800
     5.2 +++ b/src/Pure/Isar/code.ML	Fri Dec 05 00:23:37 2008 +0100
     5.3 @@ -15,7 +15,7 @@
     5.4    val add_default_eqn_attrib: Attrib.src
     5.5    val del_eqn: thm -> theory -> theory
     5.6    val del_eqns: string -> theory -> theory
     5.7 -  val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
     5.8 +  val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
     5.9    val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    5.10    val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    5.11    val add_inline: thm -> theory -> theory
    5.12 @@ -114,7 +114,7 @@
    5.13  
    5.14  (* defining equations *)
    5.15  
    5.16 -type eqns = bool * (thm * bool) list Lazy.T;
    5.17 +type eqns = bool * (thm * bool) list lazy;
    5.18    (*default flag, theorems with linear flag (perhaps lazy)*)
    5.19  
    5.20  fun pretty_lthms ctxt r = case Lazy.peek r
     6.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 04 09:12:41 2008 -0800
     6.2 +++ b/src/Pure/Isar/proof.ML	Fri Dec 05 00:23:37 2008 +0100
     6.3 @@ -115,7 +115,7 @@
     6.4    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     6.5      ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
     6.6    val is_relevant: state -> bool
     6.7 -  val future_proof: (state -> context) -> state -> context
     6.8 +  val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
     6.9  end;
    6.10  
    6.11  structure Proof: PROOF =
    6.12 @@ -990,7 +990,7 @@
    6.13    not (is_initial state) orelse
    6.14    schematic_goal state;
    6.15  
    6.16 -fun future_proof make_proof state =
    6.17 +fun future_proof proof state =
    6.18    let
    6.19      val _ = is_relevant state andalso error "Cannot fork relevant proof";
    6.20  
    6.21 @@ -1004,16 +1004,19 @@
    6.22      fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
    6.23      val this_name = ProofContext.full_bname (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
    6.24  
    6.25 -    fun make_result () = state
    6.26 +    val result_ctxt =
    6.27 +      state
    6.28        |> map_contexts (Variable.auto_fixes prop)
    6.29        |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
    6.30 -      |> make_proof
    6.31 -      |> (fn result_ctxt => ProofContext.get_fact_single result_ctxt (Facts.named this_name));
    6.32 -    val finished_goal = Goal.protect (Goal.future_result goal_ctxt make_result prop);
    6.33 -  in
    6.34 -    state
    6.35 -    |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
    6.36 -    |> global_done_proof
    6.37 -  end;
    6.38 +      |> proof;
    6.39 +
    6.40 +    val thm = result_ctxt |> Future.map (fn (_, ctxt) =>
    6.41 +      ProofContext.get_fact_single ctxt (Facts.named this_name));
    6.42 +    val finished_goal = Goal.protect (Goal.future_result goal_ctxt thm prop);
    6.43 +    val state' =
    6.44 +      state
    6.45 +      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
    6.46 +      |> global_done_proof;
    6.47 +  in (Future.map #1 result_ctxt, state') end;
    6.48  
    6.49  end;
     7.1 --- a/src/Pure/Isar/toplevel.ML	Thu Dec 04 09:12:41 2008 -0800
     7.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Dec 05 00:23:37 2008 +0100
     7.3 @@ -691,45 +691,62 @@
     7.4  
     7.5  (* excursion of units, consisting of commands with proof *)
     7.6  
     7.7 +structure States = ProofDataFun
     7.8 +(
     7.9 +  type T = state list future option;
    7.10 +  fun init _ = NONE;
    7.11 +);
    7.12 +
    7.13  fun command_result tr st =
    7.14    let val st' = command tr st
    7.15    in (st', st') end;
    7.16  
    7.17 -fun unit_result immediate (tr, proof_trs) st =
    7.18 +fun proof_result immediate (tr, proof_trs) st =
    7.19    let val st' = command tr st in
    7.20      if immediate orelse null proof_trs orelse
    7.21        not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    7.22      then
    7.23        let val (states, st'') = fold_map command_result proof_trs st'
    7.24 -      in (fn () => (tr, st') :: (proof_trs ~~ states), st'') end
    7.25 +      in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end
    7.26      else
    7.27        let
    7.28          val (body_trs, end_tr) = split_last proof_trs;
    7.29 -        val body_states = ref ([]: state list);
    7.30          val finish = Context.Theory o ProofContext.theory_of;
    7.31 -        fun make_result prf =
    7.32 -          let val (states, State (result_node, _)) =
    7.33 -            (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
    7.34 -              => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
    7.35 -            |> fold_map command_result body_trs
    7.36 -            ||> command (end_tr |> set_print false)
    7.37 -          in body_states := states; presentation_context (Option.map #1 result_node) NONE end;
    7.38 -        val st'' = st'
    7.39 -          |> command (end_tr |> reset_trans |> end_proof (K (Proof.future_proof make_result)));
    7.40 -      in (fn () => (tr, st') :: (body_trs ~~ ! body_states) @ [(end_tr, st'')], st'') end
    7.41 +
    7.42 +        val future_proof = Proof.future_proof
    7.43 +          (fn prf =>
    7.44 +            Future.fork_background (fn () =>
    7.45 +              let val (states, State (result_node, _)) =
    7.46 +                (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
    7.47 +                  => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
    7.48 +                |> fold_map command_result body_trs
    7.49 +                ||> command (end_tr |> set_print false);
    7.50 +              in (states, presentation_context (Option.map #1 result_node) NONE) end))
    7.51 +          #> (fn (states, ctxt) => States.put (SOME states) ctxt);
    7.52 +
    7.53 +        val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
    7.54 +
    7.55 +        val states =
    7.56 +          (case States.get (presentation_context (SOME (node_of st'')) NONE) of
    7.57 +            NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
    7.58 +          | SOME states => states);
    7.59 +        val result = Lazy.lazy
    7.60 +          (fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]);
    7.61 +
    7.62 +      in (result, st'') end
    7.63    end;
    7.64  
    7.65 -fun excursion input =
    7.66 +fun excursion input = exception_trace (fn () =>
    7.67    let
    7.68      val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
    7.69  
    7.70      val immediate = not (Future.enabled ());
    7.71 -    val (future_results, end_state) = fold_map (unit_result immediate) input toplevel;
    7.72 +    val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
    7.73      val _ =
    7.74        (case end_state of
    7.75 -        State (NONE, SOME (Theory (Context.Theory thy, _), _)) => Thm.join_futures thy
    7.76 +        State (NONE, SOME (Theory (Context.Theory thy, _), _)) => PureThy.force_proofs thy
    7.77        | _ => error "Unfinished development at end of input");
    7.78 -    val results = maps (fn res => res ()) future_results;
    7.79 -  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end;
    7.80 +    val results = maps Lazy.force future_results;
    7.81 +  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);
    7.82  
    7.83  end;
     8.1 --- a/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Dec 04 09:12:41 2008 -0800
     8.2 +++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Fri Dec 05 00:23:37 2008 +0100
     8.3 @@ -4,13 +4,13 @@
     8.4  Extra toplevel pretty-printing for Poly/ML.
     8.5  *)
     8.6  
     8.7 -install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Future.T) =>
     8.8 +install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
     8.9    (case Future.peek x of
    8.10      NONE => str "<future>"
    8.11    | SOME (Exn.Exn _) => str "<failed>"
    8.12    | SOME (Exn.Result y) => print (y, depth)));
    8.13  
    8.14 -install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Lazy.T) =>
    8.15 +install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
    8.16    (case Lazy.peek x of
    8.17      NONE => str "<lazy>"
    8.18    | SOME (Exn.Exn _) => str "<failed>"
     9.1 --- a/src/Pure/Thy/thy_info.ML	Thu Dec 04 09:12:41 2008 -0800
     9.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Dec 05 00:23:37 2008 +0100
     9.3 @@ -320,14 +320,12 @@
     9.4      val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
     9.5        (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
     9.6  
     9.7 -    val group = TaskQueue.new_group ();
     9.8      fun future (name, body) tab =
     9.9        let
    9.10          val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
    9.11 -        val x = Future.future (SOME group) deps true body;
    9.12 -      in (x, Symtab.update (name, Future.task_of x) tab) end;
    9.13 +        val x = Future.fork_deps deps body;
    9.14 +      in (x, Symtab.update (name, x) tab) end;
    9.15      val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
    9.16 -    val _ = List.app (PureThy.force_proofs o get_theory o #1) tasks;
    9.17    in () end;
    9.18  
    9.19  local
    9.20 @@ -589,8 +587,6 @@
    9.21  
    9.22  (* finish all theories *)
    9.23  
    9.24 -fun finish () = change_thys (Graph.map_nodes
    9.25 -  (fn (SOME _, SOME thy) => (NONE, (PureThy.force_proofs thy; SOME thy))
    9.26 -    | (_, entry) => (NONE, entry)));
    9.27 +fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
    9.28  
    9.29  end;
    10.1 --- a/src/Pure/goal.ML	Thu Dec 04 09:12:41 2008 -0800
    10.2 +++ b/src/Pure/goal.ML	Fri Dec 05 00:23:37 2008 +0100
    10.3 @@ -20,7 +20,7 @@
    10.4    val conclude: thm -> thm
    10.5    val finish: thm -> thm
    10.6    val norm_result: thm -> thm
    10.7 -  val future_result: Proof.context -> (unit -> thm) -> term -> thm
    10.8 +  val future_result: Proof.context -> thm future -> term -> thm
    10.9    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   10.10    val prove_multi: Proof.context -> string list -> term list -> term list ->
   10.11      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   10.12 @@ -116,11 +116,11 @@
   10.13  
   10.14      val global_prop =
   10.15        Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
   10.16 -    val global_result =
   10.17 -      Thm.generalize (map #1 tfrees, []) 0 o
   10.18 -      Drule.forall_intr_list fixes o
   10.19 -      Drule.implies_intr_list assms o
   10.20 -      Thm.adjust_maxidx_thm ~1 o result;
   10.21 +    val global_result = result |> Future.map
   10.22 +      (Thm.adjust_maxidx_thm ~1 #>
   10.23 +        Drule.implies_intr_list assms #>
   10.24 +        Drule.forall_intr_list fixes #>
   10.25 +        Thm.generalize (map #1 tfrees, []) 0);
   10.26      val local_result =
   10.27        Thm.future global_result (cert global_prop)
   10.28        |> Thm.instantiate (instT, [])
   10.29 @@ -178,7 +178,7 @@
   10.30            end);
   10.31      val res =
   10.32        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
   10.33 -      else future_result ctxt' result (Thm.term_of stmt);
   10.34 +      else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
   10.35    in
   10.36      Conjunction.elim_balanced (length props) res
   10.37      |> map (Assumption.export false ctxt' ctxt)
    11.1 --- a/src/Pure/proofterm.ML	Thu Dec 04 09:12:41 2008 -0800
    11.2 +++ b/src/Pure/proofterm.ML	Fri Dec 05 00:23:37 2008 +0100
    11.3 @@ -22,10 +22,10 @@
    11.4     | PAxm of string * term * typ list option
    11.5     | Oracle of string * term * typ list option
    11.6     | Promise of serial * term * typ list
    11.7 -   | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
    11.8 +   | PThm of serial * ((string * term * typ list option) * proof_body lazy)
    11.9    and proof_body = PBody of
   11.10      {oracles: (string * term) OrdList.T,
   11.11 -     thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
   11.12 +     thms: (serial * (string * term * proof_body lazy)) OrdList.T,
   11.13       proof: proof}
   11.14  
   11.15    val %> : proof * term -> proof
   11.16 @@ -36,10 +36,10 @@
   11.17    include BASIC_PROOFTERM
   11.18  
   11.19    type oracle = string * term
   11.20 -  type pthm = serial * (string * term * proof_body Lazy.T)
   11.21 -  val force_body: proof_body Lazy.T ->
   11.22 +  type pthm = serial * (string * term * proof_body lazy)
   11.23 +  val force_body: proof_body lazy ->
   11.24      {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
   11.25 -  val force_proof: proof_body Lazy.T -> proof
   11.26 +  val force_proof: proof_body lazy -> proof
   11.27    val proof_of: proof_body -> proof
   11.28    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   11.29    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   11.30 @@ -111,7 +111,7 @@
   11.31    val promise_proof: theory -> serial -> term -> proof
   11.32    val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
   11.33    val thm_proof: theory -> string -> term list -> term ->
   11.34 -    (serial * proof) list Lazy.T -> proof_body -> pthm * proof
   11.35 +    (serial * proof) list lazy -> proof_body -> pthm * proof
   11.36    val get_name: term list -> term -> proof -> string
   11.37  
   11.38    (** rewriting on proof terms **)
   11.39 @@ -143,14 +143,14 @@
   11.40   | PAxm of string * term * typ list option
   11.41   | Oracle of string * term * typ list option
   11.42   | Promise of serial * term * typ list
   11.43 - | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
   11.44 + | PThm of serial * ((string * term * typ list option) * proof_body lazy)
   11.45  and proof_body = PBody of
   11.46    {oracles: (string * term) OrdList.T,
   11.47 -   thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
   11.48 +   thms: (serial * (string * term * proof_body lazy)) OrdList.T,
   11.49     proof: proof};
   11.50  
   11.51  type oracle = string * term;
   11.52 -type pthm = serial * (string * term * proof_body Lazy.T);
   11.53 +type pthm = serial * (string * term * proof_body lazy);
   11.54  
   11.55  val force_body = Lazy.force #> (fn PBody args => args);
   11.56  val force_proof = #proof o force_body;
    12.1 --- a/src/Pure/pure_thy.ML	Thu Dec 04 09:12:41 2008 -0800
    12.2 +++ b/src/Pure/pure_thy.ML	Fri Dec 05 00:23:37 2008 +0100
    12.3 @@ -59,7 +59,7 @@
    12.4  
    12.5  structure FactsData = TheoryDataFun
    12.6  (
    12.7 -  type T = Facts.T * unit Lazy.T list;
    12.8 +  type T = Facts.T * unit lazy list;
    12.9    val empty = (Facts.empty, []);
   12.10    val copy = I;
   12.11    fun extend (facts, _) = (facts, []);
   12.12 @@ -80,7 +80,9 @@
   12.13  (* proofs *)
   12.14  
   12.15  fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
   12.16 -val force_proofs = List.app Lazy.force o #2 o FactsData.get;
   12.17 +
   12.18 +fun force_proofs thy =
   12.19 +  ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
   12.20  
   12.21  
   12.22  
    13.1 --- a/src/Pure/thm.ML	Thu Dec 04 09:12:41 2008 -0800
    13.2 +++ b/src/Pure/thm.ML	Fri Dec 05 00:23:37 2008 +0100
    13.3 @@ -146,8 +146,7 @@
    13.4    val varifyT: thm -> thm
    13.5    val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
    13.6    val freezeT: thm -> thm
    13.7 -  val join_futures: theory -> unit
    13.8 -  val future: (unit -> thm) -> cterm -> thm
    13.9 +  val future: thm future -> cterm -> thm
   13.10    val proof_body_of: thm -> proof_body
   13.11    val proof_of: thm -> proof
   13.12    val force_proof: thm -> unit
   13.13 @@ -347,8 +346,8 @@
   13.14    tpairs: (term * term) list,                   (*flex-flex pairs*)
   13.15    prop: term}                                   (*conclusion*)
   13.16  and deriv = Deriv of
   13.17 - {all_promises: (serial * thm Future.T) OrdList.T,
   13.18 -  promises: (serial * thm Future.T) OrdList.T,
   13.19 + {all_promises: (serial * thm future) OrdList.T,
   13.20 +  promises: (serial * thm future) OrdList.T,
   13.21    body: Pt.proof_body};
   13.22  
   13.23  type conv = cterm -> thm;
   13.24 @@ -1587,36 +1586,7 @@
   13.25  
   13.26  
   13.27  
   13.28 -(*** Promises ***)
   13.29 -
   13.30 -(* pending future derivations *)
   13.31 -
   13.32 -structure Futures = TheoryDataFun
   13.33 -(
   13.34 -  type T = thm Future.T list ref;
   13.35 -  val empty : T = ref [];
   13.36 -  val copy = I;  (*shared ref within all versions of whole theory body*)
   13.37 -  fun extend _ : T = ref [];
   13.38 -  fun merge _ _ : T = ref [];
   13.39 -);
   13.40 -
   13.41 -val _ = Context.>> (Context.map_theory Futures.init);
   13.42 -
   13.43 -fun add_future thy future = CRITICAL (fn () => change (Futures.get thy) (cons future));
   13.44 -
   13.45 -fun join_futures thy =
   13.46 -  let
   13.47 -    val futures = Futures.get thy;
   13.48 -    fun joined () =
   13.49 -     (List.app (ignore o Future.join_result) (rev (! futures));
   13.50 -      CRITICAL (fn () =>
   13.51 -        let
   13.52 -          val (finished, unfinished) = List.partition Future.is_finished (! futures);
   13.53 -          val _ = futures := unfinished;
   13.54 -        in finished end)
   13.55 -      |> Future.join_results |> Exn.release_all |> null);
   13.56 -  in while not (joined ()) do () end;
   13.57 -
   13.58 +(*** Future theorems -- proofs with promises ***)
   13.59  
   13.60  (* future rule *)
   13.61  
   13.62 @@ -1635,15 +1605,14 @@
   13.63      val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies";
   13.64    in thm end;
   13.65  
   13.66 -fun future make_result ct =
   13.67 +fun future future_thm ct =
   13.68    let
   13.69      val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
   13.70      val thy = Context.reject_draft (Theory.deref thy_ref);
   13.71      val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
   13.72  
   13.73      val i = serial ();
   13.74 -    val future = Future.fork_background (future_result i thy sorts prop o norm_proof o make_result);
   13.75 -    val _ = add_future thy future;
   13.76 +    val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
   13.77      val promise = (i, future);
   13.78    in
   13.79      Thm (make_deriv [promise] [promise] [] [] (Pt.promise_proof thy i prop),
    14.1 --- a/src/Tools/code/code_ml.ML	Thu Dec 04 09:12:41 2008 -0800
    14.2 +++ b/src/Tools/code/code_ml.ML	Fri Dec 05 00:23:37 2008 +0100
    14.3 @@ -912,7 +912,7 @@
    14.4  
    14.5  structure CodeAntiqData = ProofDataFun
    14.6  (
    14.7 -  type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
    14.8 +  type T = string list * (bool * (string * (string * (string * string) list) lazy));
    14.9    fun init _ = ([], (true, ("", Lazy.value ("", []))));
   14.10  );
   14.11