# HG changeset patch
# User wenzelm
# Date 1572557656 -3600
# Node ID d86798eddc14fe3b39e9e7d70ed8e952a78acb29
# Parent  19818f99b4ae32e77eb083445c1239fd63b14a0e
more accurate proof_boxes -- from actual proof body;

diff -r 19818f99b4ae -r d86798eddc14 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu Oct 31 21:21:09 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Thu Oct 31 22:34:16 2019 +0100
@@ -254,10 +254,15 @@
 
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
-    fun proof_boxes_of thm thm_id =
-      (Thm_Deps.thm_boxes
-        {included = fn thm_id' => #serial thm_id = #serial thm_id',
-         excluded = is_some o lookup_thm_id} [thm]) @ [thm_id];
+    fun proof_boxes thm thm_id =
+      let
+        val selection =
+         {included = fn thm_id' => #serial thm_id = #serial thm_id',
+          excluded = is_some o lookup_thm_id};
+        val boxes =
+          map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm])
+            handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm]
+     in boxes @ [thm_id] end;
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
       if #serial header = #serial thm_id then ""
@@ -277,7 +282,7 @@
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = clean_thm (Thm.unconstrainT raw_thm);
-        val boxes = proof_boxes_of thm thm_id;
+        val boxes = proof_boxes thm thm_id;
 
         val proof0 =
           if export_standard_proofs then
diff -r 19818f99b4ae -r d86798eddc14 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 31 21:21:09 2019 +0100
+++ b/src/Pure/proofterm.ML	Thu Oct 31 22:34:16 2019 +0100
@@ -31,6 +31,7 @@
      proof: proof}
   type oracle = string * term option
   type thm = serial * thm_node
+  exception MIN_PROOF of unit
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
@@ -188,6 +189,8 @@
   val thm_header_id: thm_header -> thm_id
   val thm_id: thm -> thm_id
   val get_id: sort list -> term list -> term -> proof -> thm_id option
+  val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} ->
+    proof list -> (thm_header * proof) list  (*exception MIN_PROOF*)
 end
 
 structure Proofterm : PROOFTERM =
@@ -228,6 +231,8 @@
 val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
 
+exception MIN_PROOF of unit;
+
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
 
@@ -1630,8 +1635,6 @@
 
 local
 
-exception MIN_PROOF of unit;
-
 fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop;
 fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
 
@@ -2320,6 +2323,30 @@
   | SOME {name = "", ...} => NONE
   | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
 
+
+(* proof boxes: intermediate PThm nodes *)
+
+fun proof_boxes {included, excluded} proofs =
+  let
+    fun boxes_of (Abst (_, _, prf)) = boxes_of prf
+      | boxes_of (AbsP (_, _, prf)) = boxes_of prf
+      | boxes_of (prf % _) = boxes_of prf
+      | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2
+      | boxes_of (PThm (header as {serial = i, ...}, thm_body)) =
+          (fn boxes =>
+            let val thm_id = thm_header_id header in
+              if Inttab.defined boxes i orelse (excluded thm_id andalso not (included thm_id))
+              then boxes
+              else
+                let
+                  val prf' = thm_body_proof_open thm_body;
+                  val boxes' = Inttab.update (i, (header, prf')) boxes;
+                in boxes_of prf' boxes' end
+            end)
+      | boxes_of MinProof = raise MIN_PROOF ()
+      | boxes_of _ = I;
+  in Inttab.fold_rev (cons o #2) (fold boxes_of proofs Inttab.empty) [] end;
+
 end;
 
 structure Basic_Proofterm =