tuned signature;
authorwenzelm
Thu Aug 30 16:39:50 2012 +0200 (2012-08-30)
changeset 4901072808e956879
parent 49009 15381ea111ec
child 49011 9c68e43502ce
tuned signature;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/global_theory.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 15:26:37 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 16:39:50 2012 +0200
     1.3 @@ -426,11 +426,11 @@
     1.4  
     1.5  val global_theory_group =
     1.6    Sign.new_group #>
     1.7 -  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
     1.8 +  Thm.begin_recent_proofs #> Theory.checkpoint;
     1.9  
    1.10  val local_theory_group =
    1.11    Local_Theory.new_group #>
    1.12 -  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
    1.13 +  Local_Theory.raw_theory (Thm.begin_recent_proofs #> Theory.checkpoint);
    1.14  
    1.15  fun generic_theory f = transaction (fn _ =>
    1.16    (fn Theory (gthy, _) => Theory (f gthy, NONE)
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 30 15:26:37 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 30 16:39:50 2012 +0200
     2.3 @@ -357,7 +357,7 @@
     2.4    is_some (Exn.get_res (Exn.capture (fn () =>
     2.5      fst (fst (Command.memo_result (the (get_result node))))
     2.6      |> Toplevel.end_theory Position.none
     2.7 -    |> Global_Theory.join_proofs) ()));
     2.8 +    |> Thm.join_all_proofs) ()));
     2.9  
    2.10  fun stable_command exec =
    2.11    (case Exn.capture Command.memo_result exec of
    2.12 @@ -365,7 +365,7 @@
    2.13    | Exn.Res ((st, _), _) =>
    2.14        (case try Toplevel.theory_of st of
    2.15          NONE => true
    2.16 -      | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
    2.17 +      | SOME thy => is_some (Exn.get_res (Exn.capture Thm.join_recent_proofs thy))));
    2.18  
    2.19  fun make_required nodes =
    2.20    let
     3.1 --- a/src/Pure/Thy/thy_info.ML	Thu Aug 30 15:26:37 2012 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Aug 30 16:39:50 2012 +0200
     3.3 @@ -176,7 +176,7 @@
     3.4  local
     3.5  
     3.6  fun finish_thy ((thy, present, commit): result) =
     3.7 -  (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
     3.8 +  (Thm.join_all_proofs thy; Future.join present; commit (); thy);
     3.9  
    3.10  val schedule_seq =
    3.11    Graph.schedule (fn deps => fn (_, task) =>
     4.1 --- a/src/Pure/global_theory.ML	Thu Aug 30 15:26:37 2012 +0200
     4.2 +++ b/src/Pure/global_theory.ML	Thu Aug 30 16:39:50 2012 +0200
     4.3 @@ -10,9 +10,6 @@
     4.4    val intern_fact: theory -> xstring -> string
     4.5    val defined_fact: theory -> string -> bool
     4.6    val hide_fact: bool -> string -> theory -> theory
     4.7 -  val begin_recent_proofs: theory -> theory
     4.8 -  val join_recent_proofs: theory -> unit
     4.9 -  val join_proofs: theory -> unit
    4.10    val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    4.11    val get_thms: theory -> xstring -> thm list
    4.12    val get_thm: theory -> xstring -> thm
    4.13 @@ -49,42 +46,20 @@
    4.14  
    4.15  (** theory data **)
    4.16  
    4.17 -type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
    4.18 -
    4.19 -val empty_proofs: proofs = ([], Lazy.value ());
    4.20 -
    4.21 -fun add_proofs more_thms ((thms, _): proofs) =
    4.22 -  let val thms' = fold cons more_thms thms
    4.23 -  in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
    4.24 -
    4.25 -fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
    4.26 -
    4.27  structure Data = Theory_Data
    4.28  (
    4.29 -  type T = Facts.T * (proofs * proofs);  (*facts, recent proofs, all proofs of theory node*)
    4.30 -  val empty = (Facts.empty, (empty_proofs, empty_proofs));
    4.31 -  fun extend (facts, _) = (facts, snd empty);
    4.32 -  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), snd empty);
    4.33 +  type T = Facts.T;
    4.34 +  val empty = Facts.empty;
    4.35 +  val extend = I;
    4.36 +  val merge = Facts.merge;
    4.37  );
    4.38  
    4.39 -
    4.40 -(* facts *)
    4.41 -
    4.42 -val facts_of = #1 o Data.get;
    4.43 +val facts_of = Data.get;
    4.44  
    4.45  val intern_fact = Facts.intern o facts_of;
    4.46  val defined_fact = Facts.defined o facts_of;
    4.47  
    4.48 -fun hide_fact fully name = Data.map (apfst (Facts.hide fully name));
    4.49 -
    4.50 -
    4.51 -(* forked proofs *)
    4.52 -
    4.53 -fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy);
    4.54 -
    4.55 -val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs)));
    4.56 -val join_recent_proofs = force_proofs o #1 o #2 o Data.get;
    4.57 -val join_proofs = force_proofs o #2 o #2 o Data.get;
    4.58 +fun hide_fact fully name = Data.map (Facts.hide fully name);
    4.59  
    4.60  
    4.61  (** retrieve theorems **)
    4.62 @@ -149,6 +124,8 @@
    4.63  
    4.64  (* enter_thms *)
    4.65  
    4.66 +fun register_proofs thms thy = (thms, Thm.register_proofs thms thy);
    4.67 +
    4.68  fun enter_thms pre_name post_name app_att (b, thms) thy =
    4.69    if Binding.is_empty b
    4.70    then app_att thms thy |-> register_proofs
    4.71 @@ -157,8 +134,7 @@
    4.72        val name = Sign.full_name thy b;
    4.73        val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
    4.74        val thms'' = map (Thm.transfer thy') thms';
    4.75 -      val thy'' = thy'
    4.76 -        |> (Data.map o apfst) (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
    4.77 +      val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
    4.78      in (thms'', thy'') end;
    4.79  
    4.80  
    4.81 @@ -192,7 +168,7 @@
    4.82  (* add_thms_dynamic *)
    4.83  
    4.84  fun add_thms_dynamic (b, f) thy = thy
    4.85 -  |> (Data.map o apfst) (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
    4.86 +  |> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
    4.87  
    4.88  
    4.89  (* note_thmss *)
     5.1 --- a/src/Pure/more_thm.ML	Thu Aug 30 15:26:37 2012 +0200
     5.2 +++ b/src/Pure/more_thm.ML	Thu Aug 30 16:39:50 2012 +0200
     5.3 @@ -95,6 +95,10 @@
     5.4    val legacy_get_kind: thm -> string
     5.5    val kind_rule: string -> thm -> thm
     5.6    val kind: string -> attribute
     5.7 +  val register_proofs: thm list -> theory -> theory
     5.8 +  val begin_recent_proofs: theory -> theory
     5.9 +  val join_recent_proofs: theory -> unit
    5.10 +  val join_all_proofs: theory -> unit
    5.11  end;
    5.12  
    5.13  structure Thm: THM =
    5.14 @@ -466,6 +470,33 @@
    5.15  fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
    5.16  
    5.17  
    5.18 +(* forked proofs within the context *)
    5.19 +
    5.20 +type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
    5.21 +
    5.22 +val empty_proofs: proofs = ([], Lazy.value ());
    5.23 +
    5.24 +fun add_proofs more_thms ((thms, _): proofs) =
    5.25 +  let val thms' = fold cons more_thms thms
    5.26 +  in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
    5.27 +
    5.28 +fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
    5.29 +
    5.30 +structure Proofs = Theory_Data
    5.31 +(
    5.32 +  type T = proofs * proofs;  (*recent proofs, all proofs of theory node*)
    5.33 +  val empty = (empty_proofs, empty_proofs);
    5.34 +  fun extend _ = empty;
    5.35 +  fun merge _ = empty;
    5.36 +);
    5.37 +
    5.38 +val register_proofs = Proofs.map o pairself o add_proofs;
    5.39 +val begin_recent_proofs = Proofs.map (apfst (K empty_proofs));
    5.40 +
    5.41 +val join_recent_proofs = force_proofs o #1 o Proofs.get;
    5.42 +val join_all_proofs = force_proofs o #2 o Proofs.get;
    5.43 +
    5.44 +
    5.45  open Thm;
    5.46  
    5.47  end;