join_proofs: implicit exception;
removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML;
tuned;
--- a/src/Pure/pure_thy.ML Tue Jul 21 20:37:32 2009 +0200
+++ b/src/Pure/pure_thy.ML Tue Jul 21 20:37:32 2009 +0200
@@ -10,8 +10,7 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
- val join_proofs: theory -> exn list
- val cancel_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
@@ -59,11 +58,11 @@
structure FactsData = TheoryDataFun
(
- type T = Facts.T * (unit lazy list * Task_Queue.group Inttab.table);
- val empty = (Facts.empty, ([], Inttab.empty));
+ type T = Facts.T * thm list;
+ val empty = (Facts.empty, []);
val copy = I;
- fun extend (facts, _) = (facts, ([], Inttab.empty));
- fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], Inttab.empty));
+ fun extend (facts, _) = (facts, []);
+ fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
);
@@ -79,14 +78,9 @@
(* proofs *)
-fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
+fun register_proofs (thy, thms) = (FactsData.map (apsnd (append thms)) thy, thms);
-fun join_proofs thy =
- map_filter (Exn.get_exn o Lazy.force_result) (rev (#1 (#2 (FactsData.get thy))));
-
-fun cancel_proofs thy =
- Inttab.fold (fn (_, group) => fn () => Future.cancel_group group)
- (#2 (#2 (FactsData.get thy))) ();
+fun join_proofs thy = Thm.join_proofs (rev (#2 (FactsData.get thy)));
@@ -146,24 +140,15 @@
(* enter_thms *)
-val pending_groups =
- Thm.promises_of #> fold (fn (_, future) =>
- if Future.is_finished future then I
- else Inttab.update (`Task_Queue.group_id (Future.group_of future)));
-
-fun enter_proofs (thy, thms) =
- (FactsData.map (apsnd (fn (proofs, groups) =>
- (fold (cons o lazy_proof) thms proofs, fold pending_groups thms groups))) thy, thms);
-
fun enter_thms pre_name post_name app_att (b, thms) thy =
if Binding.is_empty b
- then swap (enter_proofs (app_att (thy, thms)))
+ then swap (register_proofs (app_att (thy, thms)))
else
let
val naming = Sign.naming_of thy;
val name = NameSpace.full_name naming b;
val (thy', thms') =
- enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+ register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
val thms'' = map (Thm.transfer thy') thms';
val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
in (thms'', thy'') end;