--- a/src/Pure/Thy/export_theory.scala Thu Aug 15 16:57:09 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala Thu Aug 15 18:21:12 2019 +0200
@@ -65,6 +65,7 @@
/** theory content **/
val export_prefix: String = "theory/"
+ val export_prefix_proofs: String = "proofs/"
sealed case class Theory(name: String, parents: List[String],
types: List[Type],
@@ -367,6 +368,21 @@
Fact_Multi(entity, facts)
})
+ def read_proof(
+ provider: Export.Provider,
+ theory_name: String,
+ serial: Long,
+ cache: Option[Term.Cache] = None): (Term.Term, Term.Proof) =
+ {
+ val body = provider.focus(theory_name).uncompressed_yxml(export_prefix_proofs + serial)
+ if (body.isEmpty) error("Bad proof export " + serial)
+ val (prop, proof) = XML.Decode.pair(Term_XML.Decode.term, Term_XML.Decode.proof)(body)
+ cache match {
+ case None => (prop, proof)
+ case Some(cache) => (cache.term(prop), cache.proof(proof))
+ }
+ }
+
/* type classes */