--- a/src/Pure/Isar/toplevel.ML Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Aug 30 16:39:50 2012 +0200
@@ -426,11 +426,11 @@
val global_theory_group =
Sign.new_group #>
- Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+ Thm.begin_recent_proofs #> Theory.checkpoint;
val local_theory_group =
Local_Theory.new_group #>
- Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+ Local_Theory.raw_theory (Thm.begin_recent_proofs #> Theory.checkpoint);
fun generic_theory f = transaction (fn _ =>
(fn Theory (gthy, _) => Theory (f gthy, NONE)
--- a/src/Pure/PIDE/document.ML Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/PIDE/document.ML Thu Aug 30 16:39:50 2012 +0200
@@ -357,7 +357,7 @@
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_all_proofs) ()));
fun stable_command exec =
(case Exn.capture Command.memo_result exec of
@@ -365,7 +365,7 @@
| 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))));
+ | SOME thy => is_some (Exn.get_res (Exn.capture Thm.join_recent_proofs thy))));
fun make_required nodes =
let
--- a/src/Pure/Thy/thy_info.ML Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Aug 30 16:39:50 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_all_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 15:26:37 2012 +0200
+++ b/src/Pure/global_theory.ML Thu Aug 30 16:39:50 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, 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/more_thm.ML Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/more_thm.ML Thu Aug 30 16:39:50 2012 +0200
@@ -95,6 +95,10 @@
val legacy_get_kind: thm -> string
val kind_rule: string -> thm -> thm
val kind: string -> attribute
+ val register_proofs: thm list -> theory -> theory
+ val begin_recent_proofs: theory -> theory
+ val join_recent_proofs: theory -> unit
+ val join_all_proofs: theory -> unit
end;
structure Thm: THM =
@@ -466,6 +470,33 @@
fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
+(* forked proofs within the context *)
+
+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 = Theory_Data
+(
+ type T = proofs * proofs; (*recent proofs, all proofs of theory node*)
+ val empty = (empty_proofs, empty_proofs);
+ fun extend _ = empty;
+ fun merge _ = empty;
+);
+
+val register_proofs = Proofs.map o pairself o add_proofs;
+val begin_recent_proofs = Proofs.map (apfst (K empty_proofs));
+
+val join_recent_proofs = force_proofs o #1 o Proofs.get;
+val join_all_proofs = force_proofs o #2 o Proofs.get;
+
+
open Thm;
end;