# HG changeset patch
# User wenzelm
# Date 1574505402 -3600
# Node ID 8563046f15c3f33645eb276486929de68ad1670c
# Parent  f2d848a596d1f4f548ffa9d1e5a81abd6ff823e8
clarified error: tmp file can be invalid in odd situations;

diff -r f2d848a596d1 -r 8563046f15c3 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Nov 23 11:28:15 2019 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Nov 23 11:36:42 2019 +0100
@@ -636,6 +636,9 @@
       executable: Boolean,
       compress: Boolean,
       strict: Boolean)
+    {
+      def compound_name: String = isabelle.Export.compound_name(theory_name, name)
+    }
 
     val THEORY_NAME = "theory_name"
     val EXECUTABLE = "executable"
diff -r f2d848a596d1 -r 8563046f15c3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Nov 23 11:28:15 2019 +0100
+++ b/src/Pure/Tools/build.scala	Sat Nov 23 11:36:42 2019 +0100
@@ -305,7 +305,12 @@
                     (args, path) <-
                       Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
                   } {
-                    val body = Bytes.read(path)
+                    val body =
+                      try { Bytes.read(path) }
+                      catch {
+                        case ERROR(msg) =>
+                          error("Failed to read export " + quote(args.compound_name) + "\n" + msg)
+                      }
                     path.file.delete
                     export_consumer(name, args, body)
                   }