src/Pure/pure_thy.ML
changeset 29433 c42620170fa6
parent 29423 75ac4d6ff8fb
child 29579 cb520b766e00
equal deleted inserted replaced
29432:5bb5551bef03 29433:c42620170fa6
     9   val facts_of: theory -> Facts.T
     9   val facts_of: theory -> Facts.T
    10   val intern_fact: theory -> xstring -> string
    10   val intern_fact: theory -> xstring -> string
    11   val defined_fact: theory -> string -> bool
    11   val defined_fact: theory -> string -> bool
    12   val hide_fact: bool -> string -> theory -> theory
    12   val hide_fact: bool -> string -> theory -> theory
    13   val join_proofs: theory -> exn list
    13   val join_proofs: theory -> exn list
       
    14   val cancel_proofs: theory -> unit
    14   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    15   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    15   val get_thms: theory -> xstring -> thm list
    16   val get_thms: theory -> xstring -> thm list
    16   val get_thm: theory -> xstring -> thm
    17   val get_thm: theory -> xstring -> thm
    17   val all_thms_of: theory -> (string * thm) list
    18   val all_thms_of: theory -> (string * thm) list
    18   val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
    19   val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
    56 
    57 
    57 (** theory data **)
    58 (** theory data **)
    58 
    59 
    59 structure FactsData = TheoryDataFun
    60 structure FactsData = TheoryDataFun
    60 (
    61 (
    61   type T = Facts.T * unit lazy list;
    62   type T = Facts.T * (unit lazy list * Task_Queue.group list);
    62   val empty = (Facts.empty, []);
    63   val empty = (Facts.empty, ([], []));
    63   val copy = I;
    64   val copy = I;
    64   fun extend (facts, _) = (facts, []);
    65   fun extend (facts, _) = (facts, ([], []));
    65   fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
    66   fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
    66 );
    67 );
    67 
    68 
    68 
    69 
    69 (* facts *)
    70 (* facts *)
    70 
    71 
    79 (* proofs *)
    80 (* proofs *)
    80 
    81 
    81 fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
    82 fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
    82 
    83 
    83 fun join_proofs thy =
    84 fun join_proofs thy =
    84   map_filter (Exn.get_exn o Lazy.force_result) (rev (#2 (FactsData.get thy)));
    85   map_filter (Exn.get_exn o Lazy.force_result) (rev (#1 (#2 (FactsData.get thy))));
       
    86 
       
    87 fun cancel_proofs thy = List.app Future.cancel_group (#2 (#2 (FactsData.get thy)));
    85 
    88 
    86 
    89 
    87 
    90 
    88 (** retrieve theorems **)
    91 (** retrieve theorems **)
    89 
    92 
   140 
   143 
   141 
   144 
   142 (* enter_thms *)
   145 (* enter_thms *)
   143 
   146 
   144 fun enter_proofs (thy, thms) =
   147 fun enter_proofs (thy, thms) =
   145   (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
   148   (FactsData.map (apsnd (fn (proofs, groups) =>
       
   149     (fold (cons o lazy_proof) thms proofs, fold Thm.pending_groups thms groups))) thy, thms);
   146 
   150 
   147 fun enter_thms pre_name post_name app_att (b, thms) thy =
   151 fun enter_thms pre_name post_name app_att (b, thms) thy =
   148   if Binding.is_empty b
   152   if Binding.is_empty b
   149   then swap (enter_proofs (app_att (thy, thms)))
   153   then swap (enter_proofs (app_att (thy, thms)))
   150   else let
   154   else let