# HG changeset patch
# User wenzelm
# Date 1571166335 -7200
# Node ID 84145953b2a53929f2e73b9e85ed17677b067bf0
# Parent  93767b7a8e7be24fd9b0f9da9435f122016b07d4
more support for proof terms;
clarified signature;

diff -r 93767b7a8e7b -r 84145953b2a5 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Tue Oct 15 16:41:47 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Tue Oct 15 21:05:35 2019 +0200
@@ -264,16 +264,22 @@
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = clean_thm raw_thm;
+        val thm_name = Thm.derivation_name thm;
         val raw_proof =
-          if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else Proofterm.MinProof;
-        val (prop, proof) =
+          if Proofterm.export_enabled () then
+            Thm.reconstruct_proof_of thm
+            |> thm_name <> "" ? Proofterm.expand_proof thy [(thm_name, NONE)]
+          else Proofterm.MinProof;
+        val (prop, SOME proof) =
           standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME raw_proof);
+        val proof_boxes = Proofterm.proof_boxes proof;
       in
-        (prop, (deps, proof)) |>
+        (prop, (deps, (proof, proof_boxes))) |>
           let
             open XML.Encode Term_XML.Encode;
             val encode_proof = Proofterm.encode_standard_proof consts;
-          in pair encode_prop (pair (list string) (option encode_proof)) end
+            fun encode_box {serial, theory_name} = pair int string (serial, theory_name);
+          in pair encode_prop (pair (list string) (pair encode_proof (list encode_box))) end
       end;
 
     fun buffer_export_thm (serial, thm_name) =
diff -r 93767b7a8e7b -r 84145953b2a5 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Oct 15 16:41:47 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Oct 15 21:05:35 2019 +0200
@@ -163,9 +163,8 @@
   def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
     read_pure(store, read_theory(_, _, _, cache = cache))
 
-  def read_pure_proof(store: Sessions.Store, serial: Long, cache: Option[Term.Cache] = None): Proof =
-    read_pure(store,
-      (provider, _, theory_name) => read_proof(provider, theory_name, serial, cache = cache))
+  def read_pure_proof(store: Sessions.Store, id: Thm_Id, cache: Option[Term.Cache] = None): Proof =
+    read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache))
 
 
   /* entities */
@@ -337,27 +336,49 @@
 
   /* theorems */
 
-  sealed case class Thm(entity: Entity, prop: Prop, deps: List[String], proof: Option[Term.Proof])
+  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: Term.Proof,
+    proof_boxes: List[Thm_Id])
   {
     def cache(cache: Term.Cache): Thm =
-      Thm(entity.cache(cache), prop.cache(cache), deps.map(cache.string _), proof.map(cache.proof _))
+      Thm(
+        entity.cache(cache),
+        prop.cache(cache),
+        deps.map(cache.string _),
+        cache.proof(proof),
+        proof_boxes.map(_.cache(cache)))
   }
 
   def read_thms(provider: Export.Provider): List[Thm] =
     provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.THM, tree)
-        val (prop, (deps, prf)) =
+        val (prop, (deps, (prf, prf_boxes))) =
         {
           import XML.Decode._
           import Term_XML.Decode._
-          pair(decode_prop _, pair(list(string), option(proof)))(body)
+          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(proof, list(thm_id))))(body)
         }
-        Thm(entity, prop, deps, prf)
+        Thm(entity, prop, deps, prf, prf_boxes)
       })
 
   sealed case class Proof(
-    serial: Long,
     typargs: List[(String, Term.Sort)],
     args: List[(String, Term.Typ)],
     term: Term.Term,
@@ -367,21 +388,16 @@
 
     def cache(cache: Term.Cache): Proof =
       Proof(
-        serial,
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
         cache.term(term),
         cache.proof(proof))
   }
 
-  def read_proof(
-    provider: Export.Provider,
-    theory_name: String,
-    serial: Long,
-    cache: Option[Term.Cache] = None): Proof =
+  def read_proof(provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Proof =
   {
-    val body = provider.focus(theory_name).uncompressed_yxml(export_prefix_proofs + serial)
-    if (body.isEmpty) error("Bad proof export " + serial)
+    val body = provider.focus(id.theory_name).uncompressed_yxml(export_prefix_proofs + id.serial)
+    if (body.isEmpty) error("Bad proof export " + id.serial)
 
     val (typargs, (args, (prop_body, proof_body))) =
     {
@@ -393,7 +409,7 @@
     val prop = Term_XML.Decode.term_env(env)(prop_body)
     val proof = Term_XML.Decode.proof_env(env)(proof_body)
 
-    val result = Proof(serial, typargs, args, prop, proof)
+    val result = Proof(typargs, args, prop, proof)
     cache.map(result.cache(_)) getOrElse result
   }
 
diff -r 93767b7a8e7b -r 84145953b2a5 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Oct 15 16:41:47 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Oct 15 21:05:35 2019 +0200
@@ -181,6 +181,7 @@
   type thm_id = {serial: serial, theory_name: string}
   val thm_id: thm -> thm_id
   val get_id: sort list -> term list -> term -> proof -> thm_id option
+  val proof_boxes: proof -> thm_id list
 end
 
 structure Proofterm : PROOFTERM =
@@ -2276,6 +2277,27 @@
   | SOME {name = "", ...} => NONE
   | SOME {serial, theory_name, ...} => SOME {serial = serial, theory_name = theory_name});
 
+
+(* proof boxes *)
+
+fun proof_boxes proof =
+  let
+    fun boxes_of (AbsP (_, _, prf)) = boxes_of prf
+      | boxes_of (Abst (_, _, prf)) = boxes_of prf
+      | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2
+      | boxes_of (prf % _) = boxes_of prf
+      | boxes_of (PThm ({serial = i, name = "", theory_name, ...}, thm_body)) =
+          (fn boxes =>
+            if Inttab.defined boxes i then boxes
+            else
+              let
+                val prf = thm_body_proof_raw thm_body;
+                val boxes' = Inttab.update (i, theory_name) boxes;
+              in boxes_of prf boxes' end)
+      | boxes_of _ = I;
+    val boxes = boxes_of proof Inttab.empty;
+  in Inttab.fold_rev (fn (i, thy) => cons {serial = i, theory_name = thy}) boxes [] end;
+
 end;
 
 structure Basic_Proofterm =