--- 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)
}