# HG changeset patch
# User wenzelm
# Date 1572617395 -3600
# Node ID 7abe5abb4c050da3a66f6cd80a56df6802a332e2
# Parent  a1c137961c1273690e507af4d9e946a2191ecbb1
more detailed proof term output;
tuned signature;

diff -r a1c137961c12 -r 7abe5abb4c05 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Nov 01 14:30:22 2019 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Nov 01 15:09:55 2019 +0100
@@ -14,6 +14,7 @@
   val proof_of: bool -> thm -> Proofterm.proof
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
   val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
+  val pretty_proof_boxes_of: Proof.context -> bool -> thm -> Pretty.T
 end;
 
 structure Proof_Syntax : PROOF_SYNTAX =
@@ -198,4 +199,28 @@
 fun pretty_standard_proof_of ctxt full thm =
   pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
 
+fun pretty_proof_boxes_of ctxt full thm =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val selection =
+      {included = Proofterm.this_id (Thm.derivation_id thm),
+       excluded = is_some o Global_Theory.lookup_thm_id thy}
+  in
+    Proofterm.proof_boxes selection [Thm.proof_of thm]
+    |> map (fn ({serial = i, pos, prop, ...}, proof) =>
+        let
+          val proof' = proof
+            |> full ? Proofterm.reconstruct_proof thy prop
+            |> Proofterm.forall_intr_variables prop;
+          val prop' = prop
+            |> Proofterm.forall_intr_variables_term;
+          val name = Long_Name.append "thm" (string_of_int i);
+        in
+          Pretty.item
+           [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1,
+            Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof']
+        end)
+    |> Pretty.chunks
+  end;
+
 end;
diff -r a1c137961c12 -r 7abe5abb4c05 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Nov 01 14:30:22 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Fri Nov 01 15:09:55 2019 +0100
@@ -257,7 +257,7 @@
     fun proof_boxes thm thm_id =
       let
         val selection =
-         {included = fn thm_id' => #serial thm_id = #serial thm_id',
+         {included = Proofterm.this_id (SOME 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])
diff -r a1c137961c12 -r 7abe5abb4c05 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Nov 01 14:30:22 2019 +0100
+++ b/src/Pure/proofterm.ML	Fri Nov 01 15:09:55 2019 +0100
@@ -191,6 +191,7 @@
   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 this_id: thm_id option -> thm_id -> bool
   val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} ->
     proof list -> (thm_header * proof) list  (*exception MIN_PROOF*)
 end
@@ -853,8 +854,9 @@
   let val U = Term.itselfT T --> propT
   in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
 
-fun term_of _ (PThm ({name, types = Ts, ...}, _)) =
-      fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT))
+fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
+      fold AppT (these Ts)
+        (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
   | term_of _ (PAxm (name, _, Ts)) =
       fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
   | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
@@ -2325,6 +2327,9 @@
   | SOME {name = "", ...} => NONE
   | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
 
+fun this_id NONE _ = false
+  | this_id (SOME (thm_id: thm_id)) (thm_id': thm_id) = #serial thm_id = #serial thm_id';
+
 
 (* proof boxes: intermediate PThm nodes *)