diff --git a/src/Pure/PIDE/markup.scala b/src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala
+++ b/src/Pure/PIDE/markup.scala
@@ -1,739 +1,741 @@
 /*  Title:      Pure/PIDE/markup.scala
     Author:     Makarius
 
 Quasi-abstract markup elements.
 */
 
 package isabelle
 
 
 object Markup
 {
   /* elements */
 
   object Elements
   {
     def apply(elems: Set[String]): Elements = new Elements(elems)
     def apply(elems: String*): Elements = apply(Set(elems: _*))
     val empty: Elements = apply()
     val full: Elements =
       new Elements(Set.empty)
       {
         override def apply(elem: String): Boolean = true
         override def toString: String = "Elements.full"
       }
   }
 
   sealed class Elements private[Markup](private val rep: Set[String])
   {
     def apply(elem: String): Boolean = rep.contains(elem)
     def + (elem: String): Elements = new Elements(rep + elem)
     def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     def - (elem: String): Elements = new Elements(rep - elem)
     def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     override def toString: String = rep.mkString("Elements(", ",", ")")
   }
 
 
   /* properties */
 
   val NAME = "name"
   val Name = new Properties.String(NAME)
 
   val XNAME = "xname"
   val XName = new Properties.String(XNAME)
 
   val KIND = "kind"
   val Kind = new Properties.String(KIND)
 
   val CONTENT = "content"
   val Content = new Properties.String(CONTENT)
 
   val SERIAL = "serial"
   val Serial = new Properties.Long(SERIAL)
 
   val INSTANCE = "instance"
   val Instance = new Properties.String(INSTANCE)
 
 
   /* basic markup */
 
   val Empty: Markup = Markup("", Nil)
   val Broken: Markup = Markup("broken", Nil)
 
   class Markup_String(val name: String, prop: String)
   {
     private val Prop = new Properties.String(prop)
 
     def apply(s: String): Markup = Markup(name, Prop(s))
     def unapply(markup: Markup): Option[String] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
   class Markup_Int(val name: String, prop: String)
   {
     private val Prop = new Properties.Int(prop)
 
     def apply(i: Int): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
   class Markup_Long(val name: String, prop: String)
   {
     private val Prop = new Properties.Long(prop)
 
     def apply(i: Long): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Long] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
 
   /* meta data */
 
   val META_TITLE = "meta_title"
   val META_CREATOR = "meta_creator"
   val META_CONTRIBUTOR = "meta_contributor"
   val META_DATE = "meta_date"
   val META_LICENSE = "meta_license"
   val META_DESCRIPTION = "meta_description"
 
 
   /* formal entities */
 
   val BINDING = "binding"
   val ENTITY = "entity"
 
   val Def = new Properties.Long("def")
   val Ref = new Properties.Long("ref")
 
   object Entity
   {
     object Def
     {
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None
     }
     object Ref
     {
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
     }
     object Occ
     {
       def unapply(markup: Markup): Option[Long] =
         Def.unapply(markup) orElse Ref.unapply(markup)
     }
 
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) =>
           val kind = Kind.unapply(props).getOrElse("")
           val name = Name.unapply(props).getOrElse("")
           Some((kind, name))
         case _ => None
       }
   }
 
 
   /* completion */
 
   val COMPLETION = "completion"
   val NO_COMPLETION = "no_completion"
 
   val UPDATE = "update"
 
 
   /* position */
 
   val LINE = "line"
   val END_LINE = "line"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
   val POSITION = "position"
 
 
   /* expression */
 
   val EXPRESSION = "expression"
   object Expression
   {
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(EXPRESSION, Kind(kind)) => Some(kind)
         case Markup(EXPRESSION, _) => Some("")
         case _ => None
       }
   }
 
 
   /* citation */
 
   val CITATION = "citation"
   val Citation = new Markup_String(CITATION, NAME)
 
 
   /* embedded languages */
 
   val Symbols = new Properties.Boolean("symbols")
   val Antiquotes = new Properties.Boolean("antiquotes")
   val Delimited = new Properties.Boolean("delimited")
 
   val LANGUAGE = "language"
   object Language
   {
     val DOCUMENT = "document"
     val ML = "ML"
     val SML = "SML"
     val PATH = "path"
     val UNKNOWN = "unknown"
 
     def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
       markup match {
         case Markup(LANGUAGE, props) =>
           (props, props, props, props) match {
             case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
               Some((name, symbols, antiquotes, delimited))
             case _ => None
           }
         case _ => None
       }
 
     object Path
     {
       def unapply(markup: Markup): Option[Boolean] =
         markup match {
           case Language(PATH, _, _, delimited) => Some(delimited)
           case _ => None
         }
     }
   }
 
 
   /* external resources */
 
   val PATH = "path"
   val Path = new Markup_String(PATH, NAME)
 
   val EXPORT_PATH = "export_path"
   val Export_Path = new Markup_String(EXPORT_PATH, NAME)
 
   val URL = "url"
   val Url = new Markup_String(URL, NAME)
 
   val DOC = "doc"
   val Doc = new Markup_String(DOC, NAME)
 
 
   /* pretty printing */
 
   val Consistent = new Properties.Boolean("consistent")
   val Indent = new Properties.Int("indent")
   val Width = new Properties.Int("width")
 
   object Block
   {
     val name = "block"
     def apply(c: Boolean, i: Int): Markup =
       Markup(name,
         (if (c) Consistent(c) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Boolean, Int)] =
       if (markup.name == name) {
         val c = Consistent.unapply(markup.properties).getOrElse(false)
         val i = Indent.unapply(markup.properties).getOrElse(0)
         Some((c, i))
       }
       else None
   }
 
   object Break
   {
     val name = "break"
     def apply(w: Int, i: Int): Markup =
       Markup(name,
         (if (w != 0) Width(w) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Int, Int)] =
       if (markup.name == name) {
         val w = Width.unapply(markup.properties).getOrElse(0)
         val i = Indent.unapply(markup.properties).getOrElse(0)
         Some((w, i))
       }
       else None
   }
 
   val ITEM = "item"
   val BULLET = "bullet"
 
   val SEPARATOR = "separator"
 
 
   /* text properties */
 
   val WORDS = "words"
 
   val HIDDEN = "hidden"
 
   val DELETE = "delete"
 
 
   /* misc entities */
 
   val THEORY = "theory"
   val CLASS = "class"
   val TYPE_NAME = "type_name"
   val FIXED = "fixed"
   val CASE = "case"
   val CONSTANT = "constant"
   val DYNAMIC_FACT = "dynamic_fact"
 
 
   /* inner syntax */
 
   val TFREE = "tfree"
   val TVAR = "tvar"
   val FREE = "free"
   val SKOLEM = "skolem"
   val BOUND = "bound"
   val VAR = "var"
   val NUMERAL = "numeral"
   val LITERAL = "literal"
   val DELIMITER = "delimiter"
   val INNER_STRING = "inner_string"
   val INNER_CARTOUCHE = "inner_cartouche"
 
   val TOKEN_RANGE = "token_range"
 
   val SORTING = "sorting"
   val TYPING = "typing"
   val CLASS_PARAMETER = "class_parameter"
 
   val ATTRIBUTE = "attribute"
   val METHOD = "method"
 
 
   /* antiquotations */
 
   val ANTIQUOTED = "antiquoted"
   val ANTIQUOTE = "antiquote"
 
   val ML_ANTIQUOTATION = "ML_antiquotation"
   val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
   /* document text */
 
   val RAW_TEXT = "raw_text"
   val PLAIN_TEXT = "plain_text"
 
   val PARAGRAPH = "paragraph"
   val TEXT_FOLD = "text_fold"
 
   object Document_Tag
   {
     val ELEMENT = "document_tag"
     val IMPORTANT = "important"
     val UNIMPORTANT = "unimportant"
 
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(ELEMENT, Name(name)) => Some(name)
         case _ => None
       }
   }
 
 
   /* Markdown document structure */
 
   val MARKDOWN_PARAGRAPH = "markdown_paragraph"
   val MARKDOWN_ITEM = "markdown_item"
   val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
   val Markdown_List = new Markup_String("markdown_list", "kind")
 
   val ITEMIZE = "itemize"
   val ENUMERATE = "enumerate"
   val DESCRIPTION = "description"
 
 
   /* ML */
 
   val ML_KEYWORD1 = "ML_keyword1"
   val ML_KEYWORD2 = "ML_keyword2"
   val ML_KEYWORD3 = "ML_keyword3"
   val ML_DELIMITER = "ML_delimiter"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
   val ML_COMMENT = "ML_comment"
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
   val ML_STRUCTURE = "ML_structure"
   val ML_TYPING = "ML_typing"
 
   val ML_BREAKPOINT = "ML_breakpoint"
 
 
   /* outer syntax */
 
   val COMMAND = "command"
   val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"
   val KEYWORD2 = "keyword2"
   val KEYWORD3 = "keyword3"
   val QUASI_KEYWORD = "quasi_keyword"
   val IMPROPER = "improper"
   val OPERATOR = "operator"
   val STRING = "string"
   val ALT_STRING = "alt_string"
   val VERBATIM = "verbatim"
   val CARTOUCHE = "cartouche"
   val COMMENT = "comment"
 
   val LOAD_COMMAND = "load_command"
 
 
   /* comments */
 
   val COMMENT1 = "comment1"
   val COMMENT2 = "comment2"
   val COMMENT3 = "comment3"
 
 
   /* timing */
 
   val Elapsed = new Properties.Double("elapsed")
   val CPU = new Properties.Double("cpu")
   val GC = new Properties.Double("gc")
 
   object Timing_Properties
   {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
 
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {
         case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
           Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
         case _ => None
       }
 
     def parse(props: Properties.T): isabelle.Timing =
       unapply(props) getOrElse isabelle.Timing.zero
   }
 
   val TIMING = "timing"
 
   object Timing
   {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
 
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
         case _ => None
       }
   }
 
 
   /* process result */
 
   val Return_Code = new Properties.Int("return_code")
 
   object Process_Result
   {
     def apply(result: Process_Result): Properties.T =
       Return_Code(result.rc) :::
         (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
 
     def unapply(props: Properties.T): Option[Process_Result] =
       props match {
         case Return_Code(rc) =>
           val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
           Some(isabelle.Process_Result(rc, timing = timing))
         case _ => None
       }
   }
 
 
   /* command indentation */
 
   object Command_Indent
   {
     val name = "command_indent"
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Indent.unapply(markup.properties) else None
   }
 
 
   /* goals */
 
   val GOAL = "goal"
   val SUBGOAL = "subgoal"
 
 
   /* command status */
 
   val TASK = "task"
 
   val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
   val CANCELED = "canceled"
   val INITIALIZED = "initialized"
   val FINALIZED = "finalized"
   val CONSOLIDATING = "consolidating"
   val CONSOLIDATED = "consolidated"
 
 
   /* interactive documents */
 
   val VERSION = "version"
   val ASSIGN = "assign"
 
 
   /* prover process */
 
   val PROVER_COMMAND = "prover_command"
   val PROVER_ARG = "prover_arg"
 
 
   /* messages */
 
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"
   val RESULT = "result"
   val WRITELN = "writeln"
   val STATE = "state"
   val INFORMATION = "information"
   val TRACING = "tracing"
   val WARNING = "warning"
   val LEGACY = "legacy"
   val ERROR = "error"
   val NODES_STATUS = "nodes_status"
   val PROTOCOL = "protocol"
   val SYSTEM = "system"
   val STDOUT = "stdout"
   val STDERR = "stderr"
   val EXIT = "exit"
 
   val WRITELN_MESSAGE = "writeln_message"
   val STATE_MESSAGE = "state_message"
   val INFORMATION_MESSAGE = "information_message"
   val TRACING_MESSAGE = "tracing_message"
   val WARNING_MESSAGE = "warning_message"
   val LEGACY_MESSAGE = "legacy_message"
   val ERROR_MESSAGE = "error_message"
 
   val messages = Map(
     WRITELN -> WRITELN_MESSAGE,
     STATE -> STATE_MESSAGE,
     INFORMATION -> INFORMATION_MESSAGE,
     TRACING -> TRACING_MESSAGE,
     WARNING -> WARNING_MESSAGE,
     LEGACY -> LEGACY_MESSAGE,
     ERROR -> ERROR_MESSAGE)
 
   val message: String => String = messages.withDefault((s: String) => s)
 
   val NO_REPORT = "no_report"
 
   val BAD = "bad"
 
   val INTENSIFY = "intensify"
 
 
   /* active areas */
 
   val BROWSER = "browser"
   val GRAPHVIEW = "graphview"
   val THEORY_EXPORTS = "theory_exports"
 
   val SENDBACK = "sendback"
   val PADDING = "padding"
   val PADDING_LINE = (PADDING, "line")
   val PADDING_COMMAND = (PADDING, "command")
 
   val DIALOG = "dialog"
   val Result = new Properties.String(RESULT)
 
   val JEDIT_ACTION = "jedit_action"
 
 
   /* protocol message functions */
 
   val FUNCTION = "function"
 
   class Function(val name: String)
   {
     val PROPERTY: Properties.Entry = (FUNCTION, name)
   }
 
   class Properties_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
         case PROPERTY :: args => Some(args)
         case _ => None
       }
   }
 
   class Name_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
   object ML_Statistics extends Function("ML_statistics")
   {
     def unapply(props: Properties.T): Option[(Long, String)] =
       props match {
         case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
           Some((pid, stats_dir))
         case _ => None
       }
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
   {
     val Threads = new Properties.Int("threads")
   }
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Properties_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
   object Commands_Accepted extends Function("commands_accepted")
   object Assign_Update extends Function("assign_update")
   object Removed_Versions extends Function("removed_versions")
 
   object Invoke_Scala extends Function("invoke_scala")
   {
     def unapply(props: Properties.T): Option[(String, String)] =
       props match {
         case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
 
   object Cancel_Scala extends Function("cancel_scala")
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (ID, id)) => Some(id)
         case _ => None
       }
   }
 
   val PRINT_OPERATIONS = "print_operations"
 
 
   /* export */
 
   val EXPORT = "export"
   val THEORY_NAME = "theory_name"
   val EXECUTABLE = "executable"
   val COMPRESS = "compress"
   val STRICT = "strict"
 
 
   /* debugger output */
 
   val DEBUGGER_STATE = "debugger_state"
   object Debugger_State
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
   val DEBUGGER_OUTPUT = "debugger_output"
   object Debugger_Output
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
 
   /* simplifier trace */
 
   val SIMP_TRACE_PANEL = "simp_trace_panel"
 
   val SIMP_TRACE_LOG = "simp_trace_log"
   val SIMP_TRACE_STEP = "simp_trace_step"
   val SIMP_TRACE_RECURSE = "simp_trace_recurse"
   val SIMP_TRACE_HINT = "simp_trace_hint"
   val SIMP_TRACE_IGNORE = "simp_trace_ignore"
 
   val SIMP_TRACE_CANCEL = "simp_trace_cancel"
   object Simp_Trace_Cancel
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
         case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
         case _ => None
       }
   }
 
 
   /* XML data representation */
 
   def encode: XML.Encode.T[Markup] = (markup: Markup) =>
   {
     import XML.Encode._
     pair(string, properties)((markup.name, markup.properties))
   }
 
   def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
   {
     import XML.Decode._
     val (name, props) = pair(string, properties)(body)
     Markup(name, props)
   }
 }
 
 
 sealed case class Markup(name: String, properties: Properties.T)
 {
+  def is_empty: Boolean = name.isEmpty
+
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
 
   def update_properties(more_props: Properties.T): Markup =
     if (more_props.isEmpty) this
     else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) })
 
   def + (entry: Properties.Entry): Markup =
     Markup(name, Properties.put(properties, entry))
 }
diff --git a/src/Pure/PIDE/xml.ML b/src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML
+++ b/src/Pure/PIDE/xml.ML
@@ -1,422 +1,425 @@
 (*  Title:      Pure/PIDE/xml.ML
     Author:     David Aspinall
     Author:     Stefan Berghofer
     Author:     Makarius
 
 Untyped XML trees and representation of ML values.
 *)
 
 signature XML_DATA_OPS =
 sig
   type 'a A
   type 'a T
   type 'a V
   type 'a P
   val int_atom: int A
   val bool_atom: bool A
   val unit_atom: unit A
   val properties: Properties.T T
   val string: string T
   val int: int T
   val bool: bool T
   val unit: unit T
   val pair: 'a T -> 'b T -> ('a * 'b) T
   val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   val list: 'a T -> 'a list T
   val option: 'a T -> 'a option T
   val variant: 'a V list -> 'a T
 end;
 
 signature XML =
 sig
   type attributes = (string * string) list
   datatype tree =
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
   val blob: string list -> body
+  val chunk: body -> tree
   val is_empty: tree -> bool
   val is_empty_body: body -> bool
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
   val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
   val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
   val add_content: tree -> Buffer.T -> Buffer.T
   val content_of: body -> string
   val trim_blanks: body -> body
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
   val output_markup: Markup.T -> Markup.output
   val string_of: tree -> string
   val pretty: int -> tree -> Pretty.T
   val parse_comments: string list -> unit * string list
   val parse_string : string -> string option
   val parse_element: string list -> tree * string list
   val parse_document: string list -> tree * string list
   val parse: string -> tree
   exception XML_ATOM of string
   exception XML_BODY of body
   structure Encode:
   sig
     include XML_DATA_OPS
     val tree: tree T
   end
   structure Decode:
   sig
     include XML_DATA_OPS
     val tree: tree T
   end
 end;
 
 structure XML: XML =
 struct
 
 (** XML trees **)
 
 open Output_Primitives.XML;
 
 val blob = map Text;
 
+fun chunk body = Elem (Markup.empty, body);
+
 fun is_empty (Text "") = true
   | is_empty _ = false;
 
 val is_empty_body = forall is_empty;
 
 
 (* wrapped elements *)
 
 val xml_elemN = "xml_elem";
 val xml_nameN = "xml_name";
 val xml_bodyN = "xml_body";
 
 fun wrap_elem (((a, atts), body1), body2) =
   Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
 
 fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
       if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
       then SOME (((a, atts), body1), body2) else NONE
   | unwrap_elem _ = NONE;
 
 
 (* text content *)
 
 fun add_content tree =
   (case unwrap_elem tree of
     SOME (_, ts) => fold add_content ts
   | NONE =>
       (case tree of
         Elem (_, ts) => fold add_content ts
       | Text s => Buffer.add s));
 
 fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
 
 
 (* trim blanks *)
 
 fun trim_blanks trees =
   trees |> maps
     (fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
       | Text s =>
           let val s' = s |> raw_explode |> trim Symbol.is_blank |> implode;
           in if s' = "" then [] else [Text s'] end);
 
 
 
 (** string representation **)
 
 val header = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n";
 
 
 (* escaped text *)
 
 fun decode "&lt;" = "<"
   | decode "&gt;" = ">"
   | decode "&amp;" = "&"
   | decode "&apos;" = "'"
   | decode "&quot;" = "\""
   | decode c = c;
 
 fun encode "<" = "&lt;"
   | encode ">" = "&gt;"
   | encode "&" = "&amp;"
   | encode "'" = "&apos;"
   | encode "\"" = "&quot;"
   | encode c = c;
 
 val text = translate_string encode;
 
 
 (* elements *)
 
 fun elem name atts =
   space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
 
 fun element name atts body =
   let val b = implode body in
     if b = "" then enclose "<" "/>" (elem name atts)
     else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
   end;
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
 (* output *)
 
 fun buffer_of depth tree =
   let
     fun traverse _ (Elem ((name, atts), [])) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
       | traverse d (Elem ((name, atts), ts)) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
           traverse_body d ts #>
           Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
       | traverse _ (Text s) = Buffer.add (text s)
     and traverse_body 0 _ = Buffer.add "..."
       | traverse_body d ts = fold (traverse (d - 1)) ts;
   in Buffer.empty |> traverse depth tree end;
 
 val string_of = Buffer.content o buffer_of ~1;
 
 fun pretty depth tree =
   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
 
 val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
 
 
 
 (** XML parsing **)
 
 local
 
 fun err msg (xs, _) =
   fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
 
 fun ignored _ = [];
 
 fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
 fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
 val parse_name = Scan.one name_start_char ::: Scan.many name_char;
 
 val blanks = Scan.many Symbol.is_blank;
 val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode;
 val regular = Scan.one Symbol.not_eof;
 fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x);
 
 val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
 
 val parse_cdata =
   Scan.this_string "<![CDATA[" |--
   (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
   Scan.this_string "]]>";
 
 val parse_att =
   ((parse_name >> implode) --| (blanks -- $$ "=" -- blanks)) --
   (($$ "\"" || $$ "'") :|-- (fn s =>
     (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
 
 val parse_comment =
   Scan.this_string "<!--" --
   Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
   Scan.this_string "-->" >> ignored;
 
 val parse_processing_instruction =
   Scan.this_string "<?" --
   Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
   Scan.this_string "?>" >> ignored;
 
 val parse_doctype =
   Scan.this_string "<!DOCTYPE" --
   Scan.repeat (Scan.unless ($$ ">") regular) --
   $$ ">" >> ignored;
 
 val parse_misc =
   Scan.one Symbol.is_blank >> ignored ||
   parse_processing_instruction ||
   parse_comment;
 
 val parse_optional_text =
   Scan.optional (parse_chars >> (single o Text)) [];
 
 in
 
 val parse_comments =
   blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
 
 val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
 
 fun parse_content xs =
   (parse_optional_text @@@
     Scan.repeats
       ((parse_element >> single ||
         parse_cdata >> (single o Text) ||
         parse_processing_instruction ||
         parse_comment)
       @@@ parse_optional_text)) xs
 
 and parse_element xs =
   ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
     (fn (name, _) =>
       !! (err (fn () => "Expected > or />"))
        ($$ "/" -- $$ ">" >> ignored ||
         $$ ">" |-- parse_content --|
           !! (err (fn () => "Expected </" ^ implode name ^ ">"))
               ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
     >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
 
 val parse_document =
   (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
   |-- parse_element;
 
 fun parse s =
   (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
       (blanks |-- parse_document --| blanks))) (raw_explode s) of
     (x, []) => x
   | (_, ys) => error ("XML parsing error: unprocessed input\n" ^ Symbol.beginning 100 ys));
 
 end;
 
 
 
 (** XML as data representation language **)
 
 exception XML_ATOM of string;
 exception XML_BODY of tree list;
 
 
 structure Encode =
 struct
 
 type 'a A = 'a -> string;
 type 'a T = 'a -> body;
 type 'a V = 'a -> string list * body;
 type 'a P = 'a -> string list;
 
 
 (* atomic values *)
 
 fun int_atom i = Value.print_int i;
 
 fun bool_atom false = "0"
   | bool_atom true = "1";
 
 fun unit_atom () = "";
 
 
 (* structural nodes *)
 
 fun node ts = Elem ((":", []), ts);
 
 fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
 
 fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
 
 
 (* representation of standard types *)
 
 fun tree (t: tree) = [t];
 
 fun properties props = [Elem ((":", props), [])];
 
 fun string "" = []
   | string s = [Text s];
 
 val int = string o int_atom;
 
 val bool = string o bool_atom;
 
 val unit = string o unit_atom;
 
 fun pair f g (x, y) = [node (f x), node (g y)];
 
 fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
 
 fun list f xs = map (node o f) xs;
 
 fun option _ NONE = []
   | option f (SOME x) = [node (f x)];
 
 fun variant fs x =
   [tagged (the (get_index (fn f => SOME (f x) handle General.Match => NONE) fs))];
 
 end;
 
 
 structure Decode =
 struct
 
 type 'a A = string -> 'a;
 type 'a T = body -> 'a;
 type 'a V = string list * body -> 'a;
 type 'a P = string list -> 'a;
 
 
 (* atomic values *)
 
 fun int_atom s =
   Value.parse_int s
     handle Fail _ => raise XML_ATOM s;
 
 fun bool_atom "0" = false
   | bool_atom "1" = true
   | bool_atom s = raise XML_ATOM s;
 
 fun unit_atom "" = ()
   | unit_atom s = raise XML_ATOM s;
 
 
 (* structural nodes *)
 
 fun node (Elem ((":", []), ts)) = ts
   | node t = raise XML_BODY [t];
 
 fun vector atts =
   map_index (fn (i, (a, x)) => if int_atom a = i then x else raise XML_ATOM a) atts;
 
 fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   | tagged t = raise XML_BODY [t];
 
 
 (* representation of standard types *)
 
 fun tree [t] = t
   | tree ts = raise XML_BODY ts;
 
 fun properties [Elem ((":", props), [])] = props
   | properties ts = raise XML_BODY ts;
 
 fun string [] = ""
   | string [Text s] = s
   | string ts = raise XML_BODY ts;
 
 val int = int_atom o string;
 
 val bool = bool_atom o string;
 
 val unit = unit_atom o string;
 
 fun pair f g [t1, t2] = (f (node t1), g (node t2))
   | pair _ _ ts = raise XML_BODY ts;
 
 fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   | triple _ _ _ ts = raise XML_BODY ts;
 
 fun list f ts = map (f o node) ts;
 
 fun option _ [] = NONE
   | option f [t] = SOME (f (node t))
   | option _ ts = raise XML_BODY ts;
 
 fun variant fs [t] =
       let
         val (tag, (xs, ts)) = tagged t;
         val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
       in f (xs, ts) end
   | variant _ ts = raise XML_BODY ts;
 
 end;
 
 end;
diff --git a/src/Pure/PIDE/yxml.ML b/src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML
+++ b/src/Pure/PIDE/yxml.ML
@@ -1,165 +1,167 @@
 (*  Title:      Pure/PIDE/yxml.ML
     Author:     Makarius
 
 Efficient text representation of XML trees using extra characters X
 and Y -- no escaping, may nest marked text verbatim.  Suitable for
 direct inlining into plain text.
 
 Markup <elem att="val" ...>...body...</elem> is encoded as:
 
   X Y name Y att=val ... X
   ...
   body
   ...
   X Y X
 *)
 
 signature YXML =
 sig
   val X: Symbol.symbol
   val Y: Symbol.symbol
   val embed_controls: string -> string
   val detect: string -> bool
   val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val write_body: Path.T -> XML.body -> unit
   val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
   val content_of: string -> string
   val is_wellformed: string -> bool
 end;
 
 structure YXML: YXML =
 struct
 
 (** string representation **)
 
 (* idempotent recoding of certain low ASCII control characters *)
 
 fun pseudo_utf8 c =
   if Symbol.is_ascii_control c
   then chr 192 ^ chr (128 + ord c)
   else c;
 
 fun embed_controls str =
   if exists_string Symbol.is_ascii_control str
   then translate_string pseudo_utf8 str
   else str;
 
 
 (* markers *)
 
 val X_char = Char.chr 5;
 val Y_char = Char.chr 6;
 
 val X = String.str X_char;
 val Y = String.str Y_char;
 val XY = X ^ Y;
 val XYX = XY ^ X;
 
 fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
 
 
 (* output *)
 
 fun traverse string =
   let
     fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
-    fun tree (XML.Elem ((name, atts), ts)) =
-          string XY #> string name #> fold attrib atts #> string X #>
-          fold tree ts #>
-          string XYX
+    fun tree (XML.Elem (markup as (name, atts), ts)) =
+          if Markup.is_empty markup then fold tree ts
+          else
+            string XY #> string name #> fold attrib atts #> string X #>
+            fold tree ts #>
+            string XYX
       | tree (XML.Text s) = string s;
   in tree end;
 
 fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
 val string_of = string_of_body o single;
 
 fun write_body path body =
   path |> File.open_output (fn file =>
     fold (traverse (fn s => fn () => File.output file s)) body ());
 
 
 (* markup elements *)
 
 val Z = chr 0;
 val Z_text = [XML.Text Z];
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun output_markup_elem markup =
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
   in ((bg1, bg2), en) end;
 
 
 
 (** efficient YXML parsing **)
 
 local
 
 (* splitting *)
 
 val split_string =
   Substring.full #>
   Substring.tokens (fn c => c = X_char) #>
   map (Substring.fields (fn c => c = Y_char) #> map Substring.string);
 
 
 (* structural errors *)
 
 fun err msg = raise Fail ("Malformed YXML: " ^ msg);
 fun err_attribute () = err "bad attribute";
 fun err_element () = err "bad element";
 fun err_unbalanced "" = err "unbalanced element"
   | err_unbalanced name = err ("unbalanced element " ^ quote name);
 
 
 (* stack operations *)
 
 fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
 
 fun push "" _ _ = err_element ()
   | push name atts pending = ((name, atts), []) :: pending;
 
 fun pop ((("", _), _) :: _) = err_unbalanced ""
   | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
 
 
 (* parsing *)
 
 fun parse_attrib s =
   (case first_field "=" s of
     NONE => err_attribute ()
   | SOME ("", _) => err_attribute ()
   | SOME att => att);
 
 fun parse_chunk ["", ""] = pop
   | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
   | parse_chunk txts = fold (add o XML.Text) txts;
 
 in
 
 fun parse_body source =
   (case fold parse_chunk (split_string source) [(("", []), [])] of
     [(("", _), result)] => rev result
   | ((name, _), _) :: _ => err_unbalanced name);
 
 fun parse source =
   (case parse_body source of
     [result] => result
   | [] => XML.Text ""
   | _ => err "multiple results");
 
 end;
 
 val content_of = parse_body #> XML.content_of;
 
 fun is_wellformed s = string_of_body (parse_body s) = s
   handle Fail _ => false;
 
 end;
diff --git a/src/Pure/PIDE/yxml.scala b/src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala
+++ b/src/Pure/PIDE/yxml.scala
@@ -1,150 +1,153 @@
 /*  Title:      Pure/PIDE/yxml.scala
     Author:     Makarius
 
 Efficient text representation of XML trees.  Suitable for direct
 inlining into plain text.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 
 
 object YXML
 {
   /* chunk markers */
 
   val X = '\u0005'
   val Y = '\u0006'
 
   val is_X: Char => Boolean = _ == X
   val is_Y: Char => Boolean = _ == Y
 
   val X_string: String = X.toString
   val Y_string: String = Y.toString
   val XY_string: String = X_string + Y_string
   val XYX_string: String = XY_string + X_string
 
   def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
   def detect_elem(s: String): Boolean = s.startsWith(XY_string)
 
 
   /* string representation */
 
   def traversal(string: String => Unit, body: XML.Body): Unit =
   {
     def tree(t: XML.Tree): Unit =
       t match {
-        case XML.Elem(Markup(name, atts), ts) =>
-          string(XY_string)
-          string(name)
-          for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
-          string(X_string)
-          ts.foreach(tree)
-          string(XYX_string)
+        case XML.Elem(markup @ Markup(name, atts), ts) =>
+          if (markup.is_empty) ts.foreach(tree)
+          else {
+            string(XY_string)
+            string(name)
+            for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
+            string(X_string)
+            ts.foreach(tree)
+            string(XYX_string)
+          }
         case XML.Text(text) => string(text)
       }
     body.foreach(tree)
   }
 
   def string_of_body(body: XML.Body): String =
   {
     val s = new StringBuilder
     traversal(str => s ++= str, body)
     s.toString
   }
 
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
   /* parsing */
 
   private def err(msg: String) = error("Malformed YXML: " + msg)
   private def err_attribute() = err("bad attribute")
   private def err_element() = err("bad element")
   private def err_unbalanced(name: String) =
     if (name == "") err("unbalanced element")
     else err("unbalanced element " + quote(name))
 
   private def parse_attrib(source: CharSequence): (String, String) =
   {
     val s = source.toString
     val i = s.indexOf('=')
     if (i <= 0) err_attribute()
     (s.substring(0, i), s.substring(i + 1))
   }
 
 
   def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body =
   {
     /* stack operations */
 
     def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
     var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
 
     def add(x: XML.Tree): Unit =
       (stack: @unchecked) match { case (_, body) :: _ => body += x }
 
     def push(name: String, atts: XML.Attributes): Unit =
       if (name == "") err_element()
       else stack = (cache.markup(Markup(name, atts)), buffer()) :: stack
 
     def pop(): Unit =
       (stack: @unchecked) match {
         case (Markup.Empty, _) :: _ => err_unbalanced("")
         case (markup, body) :: pending =>
           stack = pending
           add(cache.tree0(XML.Elem(markup, body.toList)))
       }
 
 
     /* parse chunks */
 
     for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) {
       if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
       else {
         Library.separated_chunks(is_Y, chunk).toList match {
           case ch :: name :: atts if ch.length == 0 =>
             push(name.toString, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(cache.tree0(XML.Text(cache.string(txt.toString))))
         }
       }
     }
     (stack: @unchecked) match {
       case List((Markup.Empty, body)) => body.toList
       case (Markup(name, _), _) :: _ => err_unbalanced(name)
     }
   }
 
   def parse(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
     parse_body(source, cache = cache) match {
       case List(result) => result
       case Nil => XML.no_text
       case _ => err("multiple XML trees")
     }
 
   def parse_elem(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
     parse_body(source, cache = cache) match {
       case List(elem: XML.Elem) => elem
       case _ => err("single XML element expected")
     }
 
 
   /* failsafe parsing */
 
   private def markup_broken(source: CharSequence) =
     XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
 
   def parse_body_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body =
   {
     try { parse_body(source, cache = cache) }
     catch { case ERROR(_) => List(markup_broken(source)) }
   }
 
   def parse_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
   {
     try { parse(source, cache = cache) }
     catch { case ERROR(_) => markup_broken(source) }
   }
 }