--- a/src/Pure/Concurrent/future.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Aug 30 22:38:12 2012 +0200
@@ -73,7 +73,6 @@
val fulfill_result: 'a future -> 'a Exn.result -> unit
val fulfill: 'a future -> 'a -> unit
val shutdown: unit -> unit
- val status: (unit -> 'a) -> 'a
val group_tasks: group -> task list
val queue_status: unit -> {ready: int, pending: int, running: int, passive: int}
end;
@@ -642,20 +641,6 @@
else ();
-(* status markup *)
-
-fun status e =
- let
- val task_props =
- (case worker_task () of
- NONE => I
- | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
- val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.forked));
- val x = e (); (*sic -- report "joined" only for success*)
- val _ = Output.status (Markup.markup_only (task_props Isabelle_Markup.joined));
- in x end;
-
-
(* queue status *)
fun group_tasks group = Task_Queue.group_tasks (! queue) group;
--- a/src/Pure/General/stack.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/General/stack.ML Thu Aug 30 22:38:12 2012 +0200
@@ -10,7 +10,9 @@
val level: 'a T -> int
val init: 'a -> 'a T
val top: 'a T -> 'a
+ val bottom: 'a T -> 'a
val map_top: ('a -> 'a) -> 'a T -> 'a T
+ val map_bottom: ('a -> 'a) -> 'a T -> 'a T
val map_all: ('a -> 'a) -> 'a T -> 'a T
val push: 'a T -> 'a T
val pop: 'a T -> 'a T (*exception List.Empty*)
@@ -27,8 +29,16 @@
fun top (x, _) = x;
+fun bottom (x, []) = x
+ | bottom (_, xs) = List.last xs;
+
fun map_top f (x, xs) = (f x, xs);
+fun map_bottom f (x, []) = (f x, [])
+ | map_bottom f (x, rest) =
+ let val (ys, z) = split_last rest
+ in (x, ys @ [f z]) end;
+
fun map_all f (x, xs) = (f x, map f xs);
fun push (x, xs) = (x, x :: xs);
--- a/src/Pure/Isar/isar_cmd.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Aug 30 22:38:12 2012 +0200
@@ -265,7 +265,7 @@
(* global endings *)
fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
-val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
+val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
--- a/src/Pure/Isar/proof.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Isar/proof.ML Thu Aug 30 22:38:12 2012 +0200
@@ -21,6 +21,9 @@
val propagate_ml_env: state -> state
val bind_terms: (indexname * term option) list -> state -> state
val put_thms: bool -> string * thm list option -> state -> state
+ val begin_proofs: state -> state
+ val register_proofs: thm list -> state -> state
+ val join_recent_proofs: state -> unit
val the_facts: state -> thm list
val the_fact: state -> thm
val set_facts: thm list -> state -> state
@@ -168,8 +171,11 @@
fun init ctxt =
State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
-fun current (State st) = Stack.top st |> (fn Node node => node);
-fun map_current f (State st) = State (Stack.map_top (map_node f) st);
+fun top (State st) = Stack.top st |> (fn Node node => node);
+fun bottom (State st) = Stack.bottom st |> (fn Node node => node);
+
+fun map_top f (State st) = State (Stack.map_top (map_node f) st);
+fun map_bottom f (State st) = State (Stack.map_bottom (map_node f) st);
fun map_all f (State st) = State (Stack.map_all (map_node f) st);
@@ -195,18 +201,21 @@
(* context *)
-val context_of = #context o current;
+val context_of = #context o top;
val theory_of = Proof_Context.theory_of o context_of;
fun map_node_context f =
map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
fun map_context f =
- map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
+ map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
fun map_context_result f state =
f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
+fun map_context_bottom f =
+ map_bottom (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
+
fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
fun propagate_ml_env state = map_contexts
@@ -216,9 +225,17 @@
val put_thms = map_context oo Proof_Context.put_thms;
+(* forked proofs *)
+
+val begin_proofs = map_context_bottom (Context.proof_map Thm.begin_proofs);
+val register_proofs = map_context_bottom o Context.proof_map o Thm.register_proofs;
+
+val join_recent_proofs = Thm.join_local_proofs o #context o bottom;
+
+
(* facts *)
-val get_facts = #facts o current;
+val get_facts = #facts o top;
fun the_facts state =
(case get_facts state of SOME facts => facts
@@ -229,7 +246,7 @@
| _ => error "Single theorem expected");
fun put_facts facts =
- map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
+ map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
put_thms true (Auto_Bind.thisN, facts);
val set_facts = put_facts o SOME;
@@ -249,8 +266,8 @@
(* mode *)
-val get_mode = #mode o current;
-fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
+val get_mode = #mode o top;
+fun put_mode mode = map_top (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
@@ -274,7 +291,7 @@
(* current goal *)
fun current_goal state =
- (case current state of
+ (case top state of
{context, goal = SOME (Goal goal), ...} => (context, goal)
| _ => error "No current goal");
@@ -285,7 +302,7 @@
else state
end;
-fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
+fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
val set_goal = put_goal o SOME;
val reset_goal = put_goal NONE;
@@ -338,7 +355,7 @@
fun pretty_state nr state =
let
- val {context = ctxt, facts, mode, goal = _} = current state;
+ val {context = ctxt, facts, mode, goal = _} = top state;
val verbose = Config.get ctxt Proof_Context.verbose;
fun levels_up 0 = ""
@@ -922,6 +939,7 @@
|> burrow (Proof_Context.export goal_ctxt outer_ctxt);
in
outer_state
+ |> register_proofs (flat results)
|> map_context (after_ctxt props)
|> pair (after_qed, results)
end;
@@ -1120,19 +1138,21 @@
local
-fun future_terminal_proof proof1 proof2 meths int state =
- if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
- then proof1 meths state
- else snd (proof2 (fn state' =>
- Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state);
+fun future_terminal_proof n proof1 proof2 meths int state =
+ if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
+ andalso not (is_relevant state)
+ then
+ snd (proof2 (fn state' =>
+ Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state)
+ else proof1 meths state;
in
fun local_future_terminal_proof x =
- future_terminal_proof local_terminal_proof local_future_proof x;
+ future_terminal_proof 2 local_terminal_proof local_future_proof x;
fun global_future_terminal_proof x =
- future_terminal_proof global_terminal_proof global_future_proof x;
+ future_terminal_proof 3 global_terminal_proof global_future_proof x;
end;
--- a/src/Pure/Isar/toplevel.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Aug 30 22:38:12 2012 +0200
@@ -53,9 +53,10 @@
val ignored: Position.T -> transition
val malformed: Position.T -> string -> transition
val is_malformed: transition -> bool
- val theory: (theory -> theory) -> transition -> transition
+ val join_recent_proofs: state -> unit
val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
val theory': (bool -> theory -> theory) -> transition -> transition
+ val theory: (theory -> theory) -> transition -> transition
val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
val end_local_theory: transition -> transition
val open_target: (generic_theory -> local_theory) -> transition -> transition
@@ -422,15 +423,21 @@
val unknown_context = imperative (fn () => warning "Unknown context");
-(* theory transitions *)
+(* forked proofs *)
+
+val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
+val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy);
-val global_theory_group =
- Sign.new_group #>
- Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+fun join_recent_proofs st =
+ (case try proof_of st of
+ SOME prf => Proof.join_recent_proofs prf
+ | NONE =>
+ (case try theory_of st of
+ SOME thy => Thm.join_recent_proofs thy
+ | NONE => ()));
-val local_theory_group =
- Local_Theory.new_group #>
- Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+
+(* theory transitions *)
fun generic_theory f = transaction (fn _ =>
(fn Theory (gthy, _) => Theory (f gthy, NONE)
@@ -439,7 +446,8 @@
fun theory' f = transaction (fn int =>
(fn Theory (Context.Theory thy, _) =>
let val thy' = thy
- |> global_theory_group
+ |> Sign.new_group
+ |> Theory.checkpoint
|> f int
|> Sign.reset_group;
in Theory (Context.Theory thy', NONE) end
@@ -478,9 +486,11 @@
fun local_theory_presentation loc f = present_transaction (fn int =>
(fn Theory (gthy, _) =>
let
- val (finish, lthy) = loc_begin loc gthy;
+ val (finish, lthy) = gthy
+ |> begin_proofs
+ |> loc_begin loc;
val lthy' = lthy
- |> local_theory_group
+ |> Local_Theory.new_group
|> f int
|> Local_Theory.reset_group;
in Theory (finish lthy', SOME lthy') end
@@ -534,15 +544,19 @@
fun local_theory_to_proof' loc f = begin_proof
(fn int => fn gthy =>
- let val (finish, lthy) = loc_begin loc gthy
- in (finish o Local_Theory.reset_group, f int (local_theory_group lthy)) end);
+ let val (finish, lthy) = gthy
+ |> begin_proofs
+ |> loc_begin loc;
+ in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
fun theory_to_proof f = begin_proof
(fn _ => fn gthy =>
(Context.Theory o Sign.reset_group o Proof_Context.theory_of,
- (case gthy of Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF)));
+ (case begin_proofs gthy of
+ Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
+ | _ => raise UNDEF)));
end;
@@ -552,12 +566,12 @@
| _ => raise UNDEF));
val present_proof = present_transaction (fn _ =>
- (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
+ (fn Proof (prf, x) => Proof (Proof_Node.apply Proof.begin_proofs prf, x)
| skip as SkipProof _ => skip
| _ => raise UNDEF));
fun proofs' f = transaction (fn int =>
- (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
+ (fn Proof (prf, x) => Proof (Proof_Node.applys (f int o Proof.begin_proofs) prf, x)
| skip as SkipProof _ => skip
| _ => raise UNDEF));
--- a/src/Pure/PIDE/document.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/PIDE/document.ML Thu Aug 30 22:38:12 2012 +0200
@@ -357,15 +357,12 @@
is_some (Exn.get_res (Exn.capture (fn () =>
fst (fst (Command.memo_result (the (get_result node))))
|> Toplevel.end_theory Position.none
- |> Global_Theory.join_proofs) ()));
+ |> Thm.join_theory_proofs) ()));
fun stable_command exec =
(case Exn.capture Command.memo_result exec of
Exn.Exn exn => not (Exn.is_interrupt exn)
- | Exn.Res ((st, _), _) =>
- (case try Toplevel.theory_of st of
- NONE => true
- | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
+ | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
fun make_required nodes =
let
--- a/src/Pure/PIDE/isabelle_markup.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Thu Aug 30 22:38:12 2012 +0200
@@ -89,6 +89,7 @@
val acceptedN: string val accepted: Markup.T
val forkedN: string val forked: Markup.T
val joinedN: string val joined: Markup.T
+ val cancelledN: string val cancelled: Markup.T
val failedN: string val failed: Markup.T
val finishedN: string val finished: Markup.T
val serialN: string
@@ -273,7 +274,7 @@
val (acceptedN, accepted) = markup_elem "accepted";
val (forkedN, forked) = markup_elem "forked";
val (joinedN, joined) = markup_elem "joined";
-
+val (cancelledN, cancelled) = markup_elem "cancelled";
val (failedN, failed) = markup_elem "failed";
val (finishedN, finished) = markup_elem "finished";
--- a/src/Pure/PIDE/isabelle_markup.scala Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Thu Aug 30 22:38:12 2012 +0200
@@ -195,6 +195,7 @@
val ACCEPTED = "accepted"
val FORKED = "forked"
val JOINED = "joined"
+ val CANCELLED = "cancelled"
val FAILED = "failed"
val FINISHED = "finished"
--- a/src/Pure/PIDE/protocol.scala Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Aug 30 22:38:12 2012 +0200
@@ -65,13 +65,14 @@
val command_status_markup: Set[String] =
Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
- Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
+ Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, Isabelle_Markup.CANCELLED)
def command_status(status: Status, markup: Markup): Status =
markup match {
case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
+ case Markup(Isabelle_Markup.CANCELLED, _) => status.copy(failed = true)
case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
case _ => status
--- a/src/Pure/Thy/thy_info.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Aug 30 22:38:12 2012 +0200
@@ -176,7 +176,7 @@
local
fun finish_thy ((thy, present, commit): result) =
- (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
+ (Thm.join_theory_proofs thy; Future.join present; commit (); thy);
val schedule_seq =
Graph.schedule (fn deps => fn (_, task) =>
--- a/src/Pure/global_theory.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/global_theory.ML Thu Aug 30 22:38:12 2012 +0200
@@ -10,9 +10,6 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
- val begin_recent_proofs: theory -> theory
- val join_recent_proofs: theory -> unit
- val join_proofs: theory -> unit
val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
@@ -49,42 +46,20 @@
(** theory data **)
-type proofs = thm list * unit lazy; (*accumulated thms, persistent join*)
-
-val empty_proofs: proofs = ([], Lazy.value ());
-
-fun add_proofs more_thms ((thms, _): proofs) =
- let val thms' = fold cons more_thms thms
- in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
-
-fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
-
structure Data = Theory_Data
(
- type T = Facts.T * (proofs * proofs); (*facts, recent proofs, all proofs of theory node*)
- val empty = (Facts.empty, (empty_proofs, empty_proofs));
- fun extend (facts, _) = (facts, snd empty);
- fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), snd empty);
+ type T = Facts.T;
+ val empty = Facts.empty;
+ val extend = I;
+ val merge = Facts.merge;
);
-
-(* facts *)
-
-val facts_of = #1 o Data.get;
+val facts_of = Data.get;
val intern_fact = Facts.intern o facts_of;
val defined_fact = Facts.defined o facts_of;
-fun hide_fact fully name = Data.map (apfst (Facts.hide fully name));
-
-
-(* forked proofs *)
-
-fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy);
-
-val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs)));
-val join_recent_proofs = force_proofs o #1 o #2 o Data.get;
-val join_proofs = force_proofs o #2 o #2 o Data.get;
+fun hide_fact fully name = Data.map (Facts.hide fully name);
(** retrieve theorems **)
@@ -149,6 +124,8 @@
(* enter_thms *)
+fun register_proofs thms thy = (thms, Context.theory_map (Thm.register_proofs thms) thy);
+
fun enter_thms pre_name post_name app_att (b, thms) thy =
if Binding.is_empty b
then app_att thms thy |-> register_proofs
@@ -157,8 +134,7 @@
val name = Sign.full_name thy b;
val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
val thms'' = map (Thm.transfer thy') thms';
- val thy'' = thy'
- |> (Data.map o apfst) (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
+ val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
in (thms'', thy'') end;
@@ -192,7 +168,7 @@
(* add_thms_dynamic *)
fun add_thms_dynamic (b, f) thy = thy
- |> (Data.map o apfst) (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
+ |> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
(* note_thmss *)
--- a/src/Pure/goal.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/goal.ML Thu Aug 30 22:38:12 2012 +0200
@@ -26,8 +26,9 @@
val norm_result: thm -> thm
val fork_name: string -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
+ val future_enabled_level: int -> bool
val future_enabled: unit -> bool
- val local_future_enabled: unit -> bool
+ val future_enabled_nested: int -> bool
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 ->
@@ -119,6 +120,24 @@
("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
in n end);
+fun capture_status e =
+ let
+ val task_props =
+ (case Future.worker_task () of
+ NONE => I
+ | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]);
+ fun status m = Output.status (Markup.markup_only (task_props m));
+
+ val _ = status Isabelle_Markup.forked;
+ val result = Exn.capture (Future.interruptible_task e) ();
+ val _ =
+ (case result of
+ Exn.Res _ => status Isabelle_Markup.joined
+ | Exn.Exn exn =>
+ if Exn.is_interrupt exn then status Isabelle_Markup.cancelled
+ else status Isabelle_Markup.failed);
+ in result end;
+
fun fork_name name e =
uninterruptible (fn _ => fn () =>
let
@@ -126,9 +145,7 @@
val future =
(singleton o Future.forks)
{name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
- (fn () =>
- Exn.release
- (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
+ (fn () => Exn.release (capture_status e before forked ~1));
in future end) ();
fun fork e = fork_name "Goal.fork" e;
@@ -139,12 +156,14 @@
val parallel_proofs = Unsynchronized.ref 1;
val parallel_proofs_threshold = Unsynchronized.ref 50;
-fun future_enabled () =
- Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso
+fun future_enabled_level n =
+ Multithreading.enabled () andalso ! parallel_proofs >= n andalso
is_some (Future.worker_task ());
-fun local_future_enabled () =
- future_enabled () andalso ! parallel_proofs >= 2 andalso
+fun future_enabled () = future_enabled_level 1;
+
+fun future_enabled_nested n =
+ future_enabled_level n andalso
Synchronized.value forked_proofs <
! parallel_proofs_threshold * Multithreading.max_threads_value ();
--- a/src/Pure/more_thm.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/more_thm.ML Thu Aug 30 22:38:12 2012 +0200
@@ -95,6 +95,11 @@
val legacy_get_kind: thm -> string
val kind_rule: string -> thm -> thm
val kind: string -> attribute
+ val register_proofs: thm list -> Context.generic -> Context.generic
+ val begin_proofs: Context.generic -> Context.generic
+ val join_local_proofs: Proof.context -> unit
+ val join_recent_proofs: theory -> unit
+ val join_theory_proofs: theory -> unit
end;
structure Thm: THM =
@@ -466,6 +471,34 @@
fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
+(* forked proofs *)
+
+type proofs = thm list * unit lazy; (*accumulated thms, persistent join*)
+
+val empty_proofs: proofs = ([], Lazy.value ());
+
+fun add_proofs more_thms ((thms, _): proofs) =
+ let val thms' = fold cons more_thms thms
+ in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
+
+fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
+
+structure Proofs = Generic_Data
+(
+ type T = proofs * proofs; (*recent proofs since last begin, all proofs of theory node*)
+ val empty = (empty_proofs, empty_proofs);
+ fun extend _ = empty;
+ fun merge _ = empty;
+);
+
+val begin_proofs = Proofs.map (apfst (K empty_proofs));
+val register_proofs = Proofs.map o pairself o add_proofs;
+
+val join_local_proofs = force_proofs o #1 o Proofs.get o Context.Proof;
+val join_recent_proofs = force_proofs o #1 o Proofs.get o Context.Theory;
+val join_theory_proofs = force_proofs o #2 o Proofs.get o Context.Theory;
+
+
open Thm;
end;
--- a/src/Pure/thm.ML Thu Aug 30 17:22:34 2012 +0200
+++ b/src/Pure/thm.ML Thu Aug 30 22:38:12 2012 +0200
@@ -514,7 +514,7 @@
fun join_promises [] = ()
| join_promises promises = join_promises_of (Future.joins (map snd promises))
-and join_promises_of thms = join_promises (maps raw_promises_of thms);
+and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));
fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body