src/Pure/thm.ML
changeset 28842 e44fae2b721d
parent 28829 c67ab5df760b
child 28847 648f01ec1794
equal deleted inserted replaced
28841:5556c7976837 28842:e44fae2b721d
   148   val freezeT: thm -> thm
   148   val freezeT: thm -> thm
   149   val join_futures: theory -> unit
   149   val join_futures: theory -> unit
   150   val future: (unit -> thm) -> cterm -> thm
   150   val future: (unit -> thm) -> cterm -> thm
   151   val proof_body_of: thm -> proof_body
   151   val proof_body_of: thm -> proof_body
   152   val proof_of: thm -> proof
   152   val proof_of: thm -> proof
       
   153   val force_proof: thm -> unit
   153   val extern_oracles: theory -> xstring list
   154   val extern_oracles: theory -> xstring list
   154   val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   155   val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   155 end;
   156 end;
   156 
   157 
   157 structure Thm:> THM =
   158 structure Thm:> THM =
  1592 
  1593 
  1593 structure Futures = TheoryDataFun
  1594 structure Futures = TheoryDataFun
  1594 (
  1595 (
  1595   type T = thm Future.T list ref;
  1596   type T = thm Future.T list ref;
  1596   val empty : T = ref [];
  1597   val empty : T = ref [];
  1597   val copy = I;  (*shared ref within whole theory body*)
  1598   val copy = I;  (*shared ref within all versions of whole theory body*)
  1598   fun extend _ : T = ref [];
  1599   fun extend _ : T = ref [];
  1599   fun merge _ _ : T = ref [];
  1600   fun merge _ _ : T = ref [];
  1600 );
  1601 );
  1601 
  1602 
  1602 val _ = Context.>> (Context.map_theory Futures.init);
  1603 val _ = Context.>> (Context.map_theory Futures.init);
  1611       CRITICAL (fn () =>
  1612       CRITICAL (fn () =>
  1612         let
  1613         let
  1613           val (finished, unfinished) = List.partition Future.is_finished (! futures);
  1614           val (finished, unfinished) = List.partition Future.is_finished (! futures);
  1614           val _ = futures := unfinished;
  1615           val _ = futures := unfinished;
  1615         in finished end)
  1616         in finished end)
  1616       |> Future.join_results |> Exn.release_all |> null);
  1617       |> Future.join_results |> null);
  1617   in while not (joined ()) do () end;
  1618   in while not (joined ()) do () end;
  1618 
  1619 
  1619 
  1620 
  1620 (* future rule *)
  1621 (* future rule *)
  1621 
  1622 
  1665     val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
  1666     val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
  1666     val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
  1667     val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
  1667   in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
  1668   in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
  1668 
  1669 
  1669 val proof_of = Proofterm.proof_of o proof_body_of;
  1670 val proof_of = Proofterm.proof_of o proof_body_of;
       
  1671 val force_proof = ignore o proof_body_of;
  1670 
  1672 
  1671 
  1673 
  1672 (* closed derivations with official name *)
  1674 (* closed derivations with official name *)
  1673 
  1675 
  1674 fun get_name thm =
  1676 fun get_name thm =