# HG changeset patch # User wenzelm # Date 1527846663 -7200 # Node ID 9e6e7ab77434a6d2768b4419b55be0e6c8b0a027 # Parent b44010800a190c9cb27618e150a86bfbb5833cac more dump aspects, with options; tuned signature; diff -r b44010800a19 -r 9e6e7ab77434 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Fri Jun 01 11:50:20 2018 +0200 +++ b/src/Pure/Tools/dump.scala Fri Jun 01 11:51:03 2018 +0200 @@ -14,40 +14,58 @@ sealed case class Aspect_Args( options: Options, progress: Progress, output_dir: Path, result: Thy_Resources.Theories_Result) { - def write(node_name: Document.Node.Name, file_name: String, bytes: Bytes) + def write(node_name: Document.Node.Name, file_name: Path, bytes: Bytes) { - val path = output_dir + Path.basic(node_name.theory) + Path.basic(file_name) + val path = output_dir + Path.basic(node_name.theory) + file_name Isabelle_System.mkdirs(path.dir) Bytes.write(path, bytes) } - def write(node_name: Document.Node.Name, file_name: String, text: String): Unit = + def write(node_name: Document.Node.Name, file_name: Path, text: String): Unit = write(node_name, file_name, Bytes(text)) - def write(node_name: Document.Node.Name, file_name: String, body: XML.Body): Unit = + def write(node_name: Document.Node.Name, file_name: Path, body: XML.Body): Unit = write(node_name, file_name, Symbol.encode(YXML.string_of_body(body))) } - sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit) + sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit, + options: List[String] = Nil) { override def toString: String = name } - private val known_aspects = + val known_aspects = List( Aspect("messages", "output messages (YXML format)", { case args => for (node_name <- args.result.node_names) { - args.write(node_name, "messages.yxml", + args.write(node_name, Path.explode("messages.yxml"), args.result.messages(node_name).iterator.map(_._1).toList) } }), Aspect("markup", "PIDE markup (YXML format)", { case args => for (node_name <- args.result.node_names) { - args.write(node_name, "markup.yxml", args.result.markup_to_XML(node_name)) + args.write(node_name, Path.explode("markup.yxml"), + args.result.markup_to_XML(node_name)) } - }) + }), + Aspect("latex", "generated LaTeX source", + { case args => + for { + node_name <- args.result.node_names + entry <- args.result.exports(node_name) + if entry.name == "document.tex" + } args.write(node_name, Path.explode(entry.name), entry.uncompressed()) + }, options = List("editor_presentation")), + Aspect("theory", "foundational theory content", + { case args => + for { + node_name <- args.result.node_names + entry <- args.result.exports(node_name) + if entry.name.startsWith(Export_Theory.export_prefix) + } args.write(node_name, Path.explode(entry.name), entry.uncompressed()) + }, options = List("editor_presentation", "export_theory")) ).sortBy(_.name) def show_aspects: String = @@ -76,7 +94,9 @@ if (Build.build_logic(options, logic, progress = progress, dirs = dirs, system_mode = system_mode) != 0) error(logic + " FAILED") - val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false) + val dump_options = + (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)( + { case (opts, aspect) => (opts /: aspect.options)(_ + _) }) /* dependencies */