--- a/src/Pure/Thy/export_theory.scala Sun Nov 03 18:53:48 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala Sun Nov 03 18:55:35 2019 +0100
@@ -7,6 +7,9 @@
package isabelle
+import scala.collection.immutable.SortedMap
+
+
object Export_Theory
{
/** session content **/
@@ -352,16 +355,12 @@
sealed case class Thm_Id(serial: Long, theory_name: String)
{
def pure: Boolean = theory_name == Thy_Header.PURE
-
- def cache(cache: Term.Cache): Thm_Id =
- Thm_Id(serial, cache.string(theory_name))
}
sealed case class Thm(
entity: Entity,
prop: Prop,
deps: List[String],
- proof_boxes: List[Thm_Id],
proof: Term.Proof)
{
def cache(cache: Term.Cache): Thm =
@@ -369,7 +368,6 @@
entity.cache(cache),
prop.cache(cache),
deps.map(cache.string _),
- proof_boxes.map(_.cache(cache)),
cache.proof(proof))
}
@@ -377,18 +375,13 @@
provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.THM, tree)
- val (prop, (deps, (prf_boxes, prf))) =
+ val (prop, deps, prf) =
{
import XML.Decode._
import Term_XML.Decode._
- def thm_id(body: XML.Body): Thm_Id =
- {
- val (serial, theory_name) = pair(long, string)(body)
- Thm_Id(serial, theory_name)
- }
- pair(decode_prop _, pair(list(string), pair(list(thm_id), proof)))(body)
+ triple(decode_prop, list(string), proof)(body)
}
- Thm(entity, prop, deps, prf_boxes, prf)
+ Thm(entity, prop, deps, prf)
})
sealed case class Proof(
@@ -428,6 +421,46 @@
}
}
+ def read_proof_boxes(
+ store: Sessions.Store,
+ provider: Export.Provider,
+ proof: Term.Proof,
+ suppress: Thm_Id => Boolean = _ => false,
+ cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] =
+ {
+ var seen = Set.empty[Long]
+ var result = SortedMap.empty[Long, (Thm_Id, Proof)]
+
+ def boxes(prf: Term.Proof)
+ {
+ prf match {
+ case Term.Abst(_, _, p) => boxes(p)
+ case Term.AbsP(_, _, p) => boxes(p)
+ case Term.Appt(p, _) => boxes(p)
+ case Term.AppP(p, q) => boxes(p); boxes(q)
+ case thm: Term.PThm if !seen(thm.serial) =>
+ seen += thm.serial
+ val id = Thm_Id(thm.serial, thm.theory_name)
+ if (!suppress(id)) {
+ val read =
+ if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache)
+ else Export_Theory.read_proof(provider, id, cache = cache)
+ read match {
+ case Some(p) =>
+ result += (thm.serial -> (id -> p))
+ boxes(p.proof)
+ case None =>
+ error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")")
+ }
+ }
+ case _ =>
+ }
+ }
+
+ boxes(proof)
+ result.iterator.map(_._2).toList
+ }
+
/* type classes */