clarified error: tmp file can be invalid in odd situations;
authorwenzelm
Sat, 23 Nov 2019 11:36:42 +0100
changeset 71351 8563046f15c3
parent 71350 f2d848a596d1
child 71352 7db80bd16f1c
clarified error: tmp file can be invalid in odd situations;
src/Pure/PIDE/markup.scala
src/Pure/Tools/build.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"
--- 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)
                   }