# HG changeset patch # User wenzelm # Date 1346359092 -7200 # Node ID 8e124393c281488312e617bb9da820a59aac6b30 # Parent b77e1910af8ac60304a5e5331c95a00cdb3015e1# Parent 1266b51f9bbc77e51dd7b65bae5e661b28359c62 merged; diff -r b77e1910af8a -r 8e124393c281 src/Pure/Concurrent/future.ML --- 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; diff -r b77e1910af8a -r 8e124393c281 src/Pure/General/stack.ML --- 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); diff -r b77e1910af8a -r 8e124393c281 src/Pure/Isar/isar_cmd.ML --- 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; diff -r b77e1910af8a -r 8e124393c281 src/Pure/Isar/proof.ML --- 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; diff -r b77e1910af8a -r 8e124393c281 src/Pure/Isar/toplevel.ML --- 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)); diff -r b77e1910af8a -r 8e124393c281 src/Pure/PIDE/document.ML --- 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 diff -r b77e1910af8a -r 8e124393c281 src/Pure/PIDE/isabelle_markup.ML --- 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"; diff -r b77e1910af8a -r 8e124393c281 src/Pure/PIDE/isabelle_markup.scala --- 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" diff -r b77e1910af8a -r 8e124393c281 src/Pure/PIDE/protocol.scala --- 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 diff -r b77e1910af8a -r 8e124393c281 src/Pure/Thy/thy_info.ML --- 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) => diff -r b77e1910af8a -r 8e124393c281 src/Pure/global_theory.ML --- 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 *) diff -r b77e1910af8a -r 8e124393c281 src/Pure/goal.ML --- 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 (); diff -r b77e1910af8a -r 8e124393c281 src/Pure/more_thm.ML --- 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; diff -r b77e1910af8a -r 8e124393c281 src/Pure/thm.ML --- 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