more operations;
more output;

--- a/src/Pure/Thy/thy_resources.scala	Tue May 29 15:04:02 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Tue May 29 17:45:48 2018 +0200
@@ -60,6 +60,7 @@
     val version: Document.Version,
     val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
   {
+    def node_names: List[Document.Node.Name] = nodes.map(_._1)
     def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
 
     def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] =
@@ -73,6 +74,13 @@
        } yield (tree, pos)).toList
     }
 
+    def markup_to_XML(node_name: Document.Node.Name,
+      range: Text.Range = Text.Range.full,
+      elements: Markup.Elements = Markup.Elements.full): XML.Body =
+    {
+      state.markup_to_XML(version, node_name, range, elements)
+    }
+
     def exports(node_name: Document.Node.Name): List[Export.Entry] =
     {
       val node = version.nodes(node_name)

--- a/src/Pure/Tools/dump.scala	Tue May 29 15:04:02 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Tue May 29 17:45:48 2018 +0200
@@ -13,17 +13,46 @@
 
   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)
+    {
+      val path = output_dir + Path.basic(node_name.theory) + Path.basic(file_name)
+      Isabelle_System.mkdirs(path.dir)
+      Bytes.write(path, bytes)
+    }
+
+    def write(node_name: Document.Node.Name, file_name: String, text: String)
+    {
+      write(node_name, file_name, Bytes(text))
+    }
+  }
 
   sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit)
 
   private val known_aspects =
     List(
       Aspect("list", "list theory nodes",
-        { case args => for ((node, _) <- args.result.nodes) args.progress.echo(node.toString) })
+        { case args =>
+            for (node_name <- args.result.node_names) args.progress.echo(node_name.toString)
+        }),
+      Aspect("messages", "output messages (YXML format)",
+        { case args =>
+            for (node_name <- args.result.node_names) {
+              args.write(node_name, "messages.yxml",
+                YXML.string_of_body(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",
+                YXML.string_of_body(args.result.markup_to_XML(node_name)))
+            }
+        })
     )
 
   def show_aspects: String =
-    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
+    cat_lines(known_aspects.sortBy(_.name).map(aspect => aspect.name + " - " + aspect.description))
 
   def the_aspect(name: String): Aspect =
     known_aspects.find(aspect => aspect.name == name) getOrElse