src/Pure/pure_thy.ML
changeset 32060 b54cb3acbbe4
parent 30853 6c6b7a72fa34
child 32105 da419b0c1c1d
equal deleted inserted replaced
32059:7991cdf10a54 32060:b54cb3acbbe4
    57 
    57 
    58 (** theory data **)
    58 (** theory data **)
    59 
    59 
    60 structure FactsData = TheoryDataFun
    60 structure FactsData = TheoryDataFun
    61 (
    61 (
    62   type T = Facts.T * (unit lazy list * Task_Queue.group list);
    62   type T = Facts.T * (unit lazy list * Task_Queue.group Inttab.table);
    63   val empty = (Facts.empty, ([], []));
    63   val empty = (Facts.empty, ([], Inttab.empty));
    64   val copy = I;
    64   val copy = I;
    65   fun extend (facts, _) = (facts, ([], []));
    65   fun extend (facts, _) = (facts, ([], Inttab.empty));
    66   fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
    66   fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], Inttab.empty));
    67 );
    67 );
    68 
    68 
    69 
    69 
    70 (* facts *)
    70 (* facts *)
    71 
    71 
    82 fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
    82 fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
    83 
    83 
    84 fun join_proofs thy =
    84 fun join_proofs thy =
    85   map_filter (Exn.get_exn o Lazy.force_result) (rev (#1 (#2 (FactsData.get thy))));
    85   map_filter (Exn.get_exn o Lazy.force_result) (rev (#1 (#2 (FactsData.get thy))));
    86 
    86 
    87 fun cancel_proofs thy = List.app Future.cancel_group (#2 (#2 (FactsData.get thy)));
    87 fun cancel_proofs thy =
       
    88   Inttab.fold (fn (_, group) => fn () => Future.cancel_group group)
       
    89     (#2 (#2 (FactsData.get thy))) ();
    88 
    90 
    89 
    91 
    90 
    92 
    91 (** retrieve theorems **)
    93 (** retrieve theorems **)
    92 
    94 
   142   burrow_fact (name_thms true official pos name) fact;
   144   burrow_fact (name_thms true official pos name) fact;
   143 
   145 
   144 
   146 
   145 (* enter_thms *)
   147 (* enter_thms *)
   146 
   148 
       
   149 val pending_groups =
       
   150   Thm.promises_of #> fold (fn (_, future) =>
       
   151     if Future.is_finished future then I
       
   152     else Inttab.update (`Task_Queue.group_id (Future.group_of future)));
       
   153 
   147 fun enter_proofs (thy, thms) =
   154 fun enter_proofs (thy, thms) =
   148   (FactsData.map (apsnd (fn (proofs, groups) =>
   155   (FactsData.map (apsnd (fn (proofs, groups) =>
   149     (fold (cons o lazy_proof) thms proofs, fold Thm.pending_groups thms groups))) thy, thms);
   156     (fold (cons o lazy_proof) thms proofs, fold pending_groups thms groups))) thy, thms);
   150 
   157 
   151 fun enter_thms pre_name post_name app_att (b, thms) thy =
   158 fun enter_thms pre_name post_name app_att (b, thms) thy =
   152   if Binding.is_empty b
   159   if Binding.is_empty b
   153   then swap (enter_proofs (app_att (thy, thms)))
   160   then swap (enter_proofs (app_att (thy, thms)))
   154   else
   161   else