--- a/src/Pure/Tools/dump.scala Mon Nov 23 13:37:10 2020 +0100
+++ b/src/Pure/Tools/dump.scala Mon Nov 23 13:52:14 2020 +0100
@@ -49,25 +49,26 @@
List(
Aspect("markup", "PIDE markup (YXML format)",
{ case args =>
- args.write(Path.explode("markup.yxml"),
+ args.write(Path.explode(Export.MARKUP),
args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
}),
Aspect("messages", "output messages (YXML format)",
{ case args =>
- args.write(Path.explode("messages.yxml"),
+ args.write(Path.explode(Export.MESSAGES),
args.snapshot.messages.iterator.map(_._1).toList)
}),
Aspect("latex", "generated LaTeX source",
{ case args =>
- for (entry <- args.snapshot.exports if entry.name.startsWith("document/")) {
- args.write(Path.explode(entry.name), entry.uncompressed())
- }
+ for {
+ entry <- args.snapshot.exports
+ if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
+ } args.write(Path.explode(entry.name), entry.uncompressed())
}),
Aspect("theory", "foundational theory content",
{ case args =>
for {
entry <- args.snapshot.exports
- if entry.name.startsWith(Export_Theory.export_prefix)
+ if entry.name_has_prefix(Export.THEORY_PREFIX)
} args.write(Path.explode(entry.name), entry.uncompressed())
}, options = List("export_theory"))
).sortBy(_.name)