# HG changeset patch
# User wenzelm
# Date 1572806639 -3600
# Node ID b05d78bfc67c80313b297225f8d4c897e8b7e9dc
# Parent  bb49abc2ecbb3afd254d3a2f805f63e56bbf6a40
clarified errors;

diff -r bb49abc2ecbb -r b05d78bfc67c src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Nov 03 18:55:35 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sun Nov 03 19:43:59 2019 +0100
@@ -431,13 +431,13 @@
     var seen = Set.empty[Long]
     var result = SortedMap.empty[Long, (Thm_Id, Proof)]
 
-    def boxes(prf: Term.Proof)
+    def boxes(context: Option[(Long, Term.Proof)], 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 Term.Abst(_, _, p) => boxes(context, p)
+        case Term.AbsP(_, _, p) => boxes(context, p)
+        case Term.Appt(p, _) => boxes(context, p)
+        case Term.AppP(p, q) => boxes(context, p); boxes(context, q)
         case thm: Term.PThm if !seen(thm.serial) =>
           seen += thm.serial
           val id = Thm_Id(thm.serial, thm.theory_name)
@@ -448,16 +448,20 @@
             read match {
               case Some(p) =>
                 result += (thm.serial -> (id -> p))
-                boxes(p.proof)
+                boxes(Some((thm.serial, p.proof)), p.proof)
               case None =>
-                error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")")
+                error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")" +
+                  (context match {
+                    case None => ""
+                    case Some((i, p)) => " in proof " + i + ":\n" + p
+                  }))
             }
           }
         case _ =>
       }
     }
 
-    boxes(proof)
+    boxes(None, proof)
     result.iterator.map(_._2).toList
   }