# HG changeset patch
# User wenzelm
# Date 1565886072 -7200
# Node ID 30b3c58a19333d851f912af8b4a9ae3b464d0519
# Parent  fc9ba6fe367f800b9d2a59ffa48e86f42c4bfbfc
support Export_Theory.read_proof, based on theory_name and serial;

diff -r fc9ba6fe367f -r 30b3c58a1933 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Aug 15 16:57:09 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 15 18:21:12 2019 +0200
@@ -390,6 +390,9 @@
     def iterator: Iterator[(Node.Name, Node)] =
       graph.iterator.map({ case (name, (node, _)) => (name, node) })
 
+    def theory_name(theory: String): Option[Node.Name] =
+      graph.keys_iterator.find(name => name.theory == theory)
+
     def commands_loading(file_name: Node.Name): List[Command] =
       (for {
         (_, node) <- iterator
diff -r fc9ba6fe367f -r 30b3c58a1933 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu Aug 15 16:57:09 2019 +0200
+++ b/src/Pure/Thy/export.scala	Thu Aug 15 18:21:12 2019 +0200
@@ -226,6 +226,10 @@
         def apply(export_name: String): Option[Entry] =
           read_entry(db, session_name, theory_name, export_name)
 
+        def focus(other_theory: String): Provider =
+          if (other_theory == theory_name) this
+          else Provider.database(db, session_name, other_theory)
+
         override def toString: String = db.toString
       }
 
@@ -234,6 +238,15 @@
         def apply(export_name: String): Option[Entry] =
           snapshot.exports_map.get(export_name)
 
+        def focus(other_theory: String): Provider =
+          if (other_theory == snapshot.node_name.theory) this
+          else {
+            val node_name =
+              snapshot.version.nodes.theory_name(other_theory) getOrElse
+                error("Bad theory " + quote(other_theory))
+            Provider.snapshot(snapshot.state.snapshot(node_name))
+          }
+
         override def toString: String = snapshot.toString
       }
 
@@ -242,6 +255,10 @@
         def apply(export_name: String): Option[Entry] =
           read_entry(dir, session_name, theory_name, export_name)
 
+        def focus(other_theory: String): Provider =
+          if (other_theory == theory_name) this
+          else Provider.directory(dir, session_name, other_theory)
+
         override def toString: String = dir.toString
       }
   }
@@ -255,6 +272,8 @@
         case Some(entry) => entry.uncompressed_yxml(cache = cache)
         case None => Nil
       }
+
+    def focus(other_theory: String): Provider
   }
 
 
diff -r fc9ba6fe367f -r 30b3c58a1933 src/Pure/Thy/export_theory.scala
--- 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 */