diff --git a/src/Pure/General/bytes.scala b/src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala
+++ b/src/Pure/General/bytes.scala
@@ -1,215 +1,218 @@
 /*  Title:      Pure/General/bytes.scala
     Author:     Makarius
 
 Immutable byte vectors versus UTF8 strings.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
   OutputStream, InputStream, FileInputStream, FileOutputStream}
 import java.net.URL
 import java.util.Base64
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
 
 object Bytes
 {
   val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
 
   def apply(s: CharSequence): Bytes =
   {
     val str = s.toString
     if (str.isEmpty) empty
     else {
       val b = UTF8.bytes(str)
       new Bytes(b, 0, b.length)
     }
   }
 
   def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)
 
   def apply(a: Array[Byte], offset: Int, length: Int): Bytes =
     if (length == 0) empty
     else {
       val b = new Array[Byte](length)
       System.arraycopy(a, offset, b, 0, length)
       new Bytes(b, 0, b.length)
     }
 
   val newline: Bytes = apply("\n")
 
   def base64(s: String): Bytes =
   {
     val a = Base64.getDecoder.decode(s)
     new Bytes(a, 0, a.length)
   }
 
 
   /* read */
 
   def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
     if (limit == 0) empty
     else {
       val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024
       val out = new ByteArrayOutputStream(out_size)
       val buf = new Array[Byte](8192)
       var m = 0
 
       do {
         m = stream.read(buf, 0, buf.length min (limit - out.size))
         if (m != -1) out.write(buf, 0, m)
       } while (m != -1 && limit > out.size)
 
       new Bytes(out.toByteArray, 0, out.size)
     }
 
   def read(file: JFile): Bytes =
   {
     val length = file.length
     val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
     using(new FileInputStream(file))(read_stream(_, limit = limit))
   }
 
   def read(path: Path): Bytes = read(path.file)
 
   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
 
 
   /* write */
 
   def write(file: JFile, bytes: Bytes): Unit =
     using(new FileOutputStream(file))(bytes.write_stream(_))
 
   def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
 }
 
 final class Bytes private(
   protected val bytes: Array[Byte],
   protected val offset: Int,
   val length: Int) extends CharSequence
 {
   /* equality */
 
   override def equals(that: Any): Boolean =
   {
     that match {
       case other: Bytes =>
         if (this eq other) true
         else if (length != other.length) false
         else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
       case _ => false
     }
   }
 
   private lazy val hash: Int =
   {
     var h = 0
     for (i <- offset until offset + length) {
       val b = bytes(i).asInstanceOf[Int] & 0xFF
       h = 31 * h + b
     }
     h
   }
 
   override def hashCode(): Int = hash
 
 
   /* content */
 
   lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
   def is_empty: Boolean = length == 0
 
   def iterator: Iterator[Byte] =
     for (i <- (offset until (offset + length)).iterator)
       yield bytes(i)
 
   def array: Array[Byte] =
   {
     val a = new Array[Byte](length)
     System.arraycopy(bytes, offset, a, 0, length)
     a
   }
 
   def text: String =
-    UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
+    UTF8.decode_chars(identity, bytes, offset, offset + length).toString
+
+  def symbols: String =
+    UTF8.decode_chars(Symbol.decode, bytes, offset, offset + length).toString
 
   def base64: String =
   {
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
     Base64.getEncoder.encodeToString(b)
   }
 
   def maybe_base64: (Boolean, String) =
   {
     val s = text
     if (this == Bytes(s)) (false, s) else (true, base64)
   }
 
   override def toString: String = "Bytes(" + length + ")"
 
   def proper: Option[Bytes] = if (is_empty) None else Some(this)
   def proper_text: Option[String] = if (is_empty) None else Some(text)
 
   def +(other: Bytes): Bytes =
     if (other.is_empty) this
     else if (is_empty) other
     else {
       val new_bytes = new Array[Byte](length + other.length)
       System.arraycopy(bytes, offset, new_bytes, 0, length)
       System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
       new Bytes(new_bytes, 0, new_bytes.length)
     }
 
 
   /* CharSequence operations */
 
   def charAt(i: Int): Char =
     if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
     else throw new IndexOutOfBoundsException
 
   def subSequence(i: Int, j: Int): Bytes =
   {
     if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
     else throw new IndexOutOfBoundsException
   }
 
   def trim_line: Bytes =
     if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10)
       subSequence(0, length - 2)
     else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10))
       subSequence(0, length - 1)
     else this
 
 
   /* streams */
 
   def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length)
 
   def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
 
 
   /* XZ data compression */
 
   def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
     using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
 
   def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes =
   {
     val result = new ByteArrayOutputStream(length)
     using(new XZOutputStream(result, options, cache))(write_stream(_))
     new Bytes(result.toByteArray, 0, result.size)
   }
 
   def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache())
     : (Boolean, Bytes) =
   {
     val compressed = compress(options = options, cache = cache)
     if (compressed.length < length) (true, compressed) else (false, this)
   }
 }
diff --git a/src/Pure/General/output_primitives.ML b/src/Pure/General/output_primitives.ML
--- a/src/Pure/General/output_primitives.ML
+++ b/src/Pure/General/output_primitives.ML
@@ -1,81 +1,81 @@
 (*  Title:      Pure/General/output_primitives.ML
     Author:     Makarius
 
 Primitives for Isabelle output channels.
 *)
 
 signature OUTPUT_PRIMITIVES =
 sig
   structure XML:
   sig
     type attributes = (string * string) list
     datatype tree =
         Elem of (string * attributes) * tree list
       | Text of string
     type body = tree list
   end
   type output = string
   type serial = int
   type properties = (string * string) list
   val ignore_outputs: output list -> unit
   val writeln_fn: output list -> unit
   val state_fn: output list -> unit
   val information_fn: output list -> unit
   val tracing_fn: output list -> unit
   val warning_fn: output list -> unit
   val legacy_fn: output list -> unit
   val error_message_fn: serial * output list -> unit
   val system_message_fn: output list -> unit
   val status_fn: output list -> unit
   val report_fn: output list -> unit
   val result_fn: properties -> output list -> unit
-  type protocol_message_fn = properties -> XML.body -> unit
+  type protocol_message_fn = properties -> XML.body list -> unit
   val protocol_message_fn: protocol_message_fn
   val markup_fn: string * properties -> output * output
 end;
 
 structure Output_Primitives: OUTPUT_PRIMITIVES =
 struct
 
 (** XML trees **)
 
 structure XML =
 struct
 
 type attributes = (string * string) list;
 
 datatype tree =
     Elem of (string * attributes) * tree list
   | Text of string;
 
 type body = tree list;
 
 end;
 
 
 (* output *)
 
 type output = string;
 type serial = int;
 type properties = (string * string) list;
 
 fun ignore_outputs (_: output list) = ();
 
 val writeln_fn = ignore_outputs;
 val state_fn = ignore_outputs;
 val information_fn = ignore_outputs;
 val tracing_fn = ignore_outputs;
 val warning_fn = ignore_outputs;
 val legacy_fn = ignore_outputs;
 fun error_message_fn (_: serial, _: output list) = ();
 val system_message_fn = ignore_outputs;
 val status_fn = ignore_outputs;
 val report_fn = ignore_outputs;
 fun result_fn (_: properties) = ignore_outputs;
 
-type protocol_message_fn = properties -> XML.body -> unit;
+type protocol_message_fn = properties -> XML.body list -> unit;
 val protocol_message_fn: protocol_message_fn = fn _ => fn _ => ();
 
 fun markup_fn (_: string * properties) = ("", "");
 
 end;
diff --git a/src/Pure/PIDE/byte_message.ML b/src/Pure/PIDE/byte_message.ML
--- a/src/Pure/PIDE/byte_message.ML
+++ b/src/Pure/PIDE/byte_message.ML
@@ -1,110 +1,116 @@
 (*  Title:      Pure/General/byte_message.ML
     Author:     Makarius
 
 Byte-oriented messages.
 *)
 
 signature BYTE_MESSAGE =
 sig
   val write: BinIO.outstream -> string list -> unit
   val write_yxml: BinIO.outstream -> XML.tree -> unit
   val flush: BinIO.outstream -> unit
   val write_line: BinIO.outstream -> string -> unit
   val read: BinIO.instream -> int -> string
   val read_block: BinIO.instream -> int -> string option * int
   val read_line: BinIO.instream -> string option
   val write_message: BinIO.outstream -> string list -> unit
+  val write_message_yxml: BinIO.outstream -> XML.body list -> unit
   val read_message: BinIO.instream -> string list option
   val write_line_message: BinIO.outstream -> string -> unit
   val read_line_message: BinIO.instream -> string option
 end;
 
 structure Byte_Message: BYTE_MESSAGE =
 struct
 
 (* output operations *)
 
 fun write stream = List.app (File.output stream);
 
 fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree ();
 
 fun flush stream = ignore (try BinIO.flushOut stream);
 
 fun write_line stream s = (write stream [s, "\n"]; flush stream);
 
 
 (* input operations *)
 
 fun read stream n = Byte.bytesToString (BinIO.inputN (stream, n));
 
 fun read_block stream n =
   let
     val msg = read stream n;
     val len = size msg;
   in (if len = n then SOME msg else NONE, len) end;
 
 fun read_line stream =
   let
     val result = trim_line o String.implode o rev;
     fun read_body cs =
       (case BinIO.input1 stream of
         NONE => if null cs then NONE else SOME (result cs)
       | SOME b =>
           (case Byte.byteToChar b of
             #"\n" => SOME (result cs)
           | c => read_body (c :: cs)));
   in read_body [] end;
 
 
 (* messages with multiple chunks (arbitrary content) *)
 
 fun make_header ns =
   [space_implode "," (map Value.print_int ns), "\n"];
 
 fun write_message stream chunks =
   (write stream (make_header (map size chunks) @ chunks); flush stream);
 
+fun write_message_yxml stream chunks =
+  (write stream (make_header (map YXML.body_size chunks));
+   (List.app o List.app) (write_yxml stream) chunks;
+   flush stream);
+
 fun parse_header line =
   map Value.parse_nat (space_explode "," line)
     handle Fail _ => error ("Malformed message header: " ^ quote line);
 
 fun read_chunk stream n =
   (case read_block stream n of
     (SOME chunk, _) => chunk
   | (NONE, len) =>
       error ("Malformed message chunk: unexpected EOF after " ^
         string_of_int len ^ " of " ^ string_of_int n ^ " bytes"));
 
 fun read_message stream =
   read_line stream |> Option.map (parse_header #> map (read_chunk stream));
 
 
 (* hybrid messages: line or length+block (with content restriction) *)
 
 fun is_length msg =
   msg <> "" andalso forall_string Symbol.is_ascii_digit msg;
 
 fun is_terminated msg =
   let val len = size msg
   in len > 0 andalso Symbol.is_ascii_line_terminator (str (String.sub (msg, len - 1))) end;
 
 fun write_line_message stream msg =
   if is_length msg orelse is_terminated msg then
     error ("Bad content for line message:\n" ^ implode (take 100 (Symbol.explode msg)))
   else
     let val n = size msg in
       write stream
         ((if n > 100 orelse exists_string (fn s => s = "\n") msg
           then make_header [n + 1] else []) @ [msg, "\n"]);
       flush stream
     end;
 
 fun read_line_message stream =
   (case read_line stream of
     NONE => NONE
   | SOME line =>
       (case try Value.parse_nat line of
         NONE => SOME line
       | SOME n => Option.map trim_line (#1 (read_block stream n))));
 
 end;
diff --git a/src/Pure/PIDE/protocol.ML b/src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML
+++ b/src/Pure/PIDE/protocol.ML
@@ -1,177 +1,177 @@
 (*  Title:      Pure/PIDE/protocol.ML
     Author:     Makarius
 
 Protocol message formats for interactive proof documents.
 *)
 
 structure Protocol: sig end =
 struct
 
 val _ =
   Protocol_Command.define "Prover.echo"
     (fn args => List.app writeln args);
 
 val _ =
   Protocol_Command.define "Prover.stop"
     (fn rc :: msgs =>
       (List.app Output.system_message msgs;
        raise Protocol_Command.STOP (Value.parse_int rc)));
 
 val _ =
   Protocol_Command.define "Prover.options"
     (fn [options_yxml] =>
       (Options.set_default (Options.decode (YXML.parse_body options_yxml));
        Isabelle_Process.init_options_interactive ()));
 
 val _ =
   Protocol_Command.define "Prover.init_session"
     (fn [yxml] => Resources.init_session_yxml yxml);
 
 val _ =
   Protocol_Command.define "Document.define_blob"
     (fn [digest, content] => Document.change_state (Document.define_blob digest content));
 
 fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command =
   let
     open XML.Decode;
     val parents = list string parents_xml;
     val (blobs_digests, blobs_index) =
       blobs_xml |>
         let
           val message = YXML.string_of_body o Protocol_Message.command_positions id;
           val blob =
             triple string string (option string)
             #> (fn (a, b, c) => {file_node = a, src_path = Path.explode b, digest = c});
         in
           pair
             (list (variant
              [fn ([], a) => Exn.Res (blob a),
               fn ([], a) => Exn.Exn (ERROR (message a))]))
             int
         end;
     val toks = list (pair int int) toks_xml;
   in
    {command_id = Document_ID.parse id,
     name = name,
     parents = parents,
     blobs_digests = blobs_digests,
     blobs_index = blobs_index,
     tokens = toks ~~ sources}
   end;
 
 fun commands_accepted ids =
-  Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)];
+  Output.protocol_message Markup.commands_accepted [[XML.Text (space_implode "," ids)]];
 
 val _ =
   Protocol_Command.define "Document.define_command"
     (fn id :: name :: parents :: blobs :: toks :: sources =>
       let
         val command =
           decode_command id name (YXML.parse_body parents) (YXML.parse_body blobs)
             (YXML.parse_body toks) sources;
         val _ = Document.change_state (Document.define_command command);
       in commands_accepted [id] end);
 
 val _ =
   Protocol_Command.define "Document.define_commands"
     (fn args =>
       let
         fun decode arg =
           let
             open XML.Decode;
             val (id, (name, (parents_xml, (blobs_xml, (toks_xml, sources))))) =
               pair string (pair string (pair I (pair I (pair I (list string)))))
                 (YXML.parse_body arg);
           in decode_command id name parents_xml blobs_xml toks_xml sources end;
 
         val commands = map decode args;
         val _ = Document.change_state (fold Document.define_command commands);
       in commands_accepted (map (Value.print_int o #command_id) commands) end);
 
 val _ =
   Protocol_Command.define "Document.discontinue_execution"
     (fn [] => Execution.discontinue ());
 
 val _ =
   Protocol_Command.define "Document.cancel_exec"
     (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id));
 
 val _ =
   Protocol_Command.define "Document.update"
     (Future.task_context "Document.update" (Future.new_group NONE)
       (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml =>
         Document.change_state (fn state =>
           let
             val old_id = Document_ID.parse old_id_string;
             val new_id = Document_ID.parse new_id_string;
             val consolidate =
               YXML.parse_body consolidate_yxml |>
                 let open XML.Decode in list string end;
             val edits =
               edits_yxml |> map (YXML.parse_body #>
                 let open XML.Decode in
                   pair string
                     (variant
                      [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                       fn ([], a) =>
                         let
                           val (master, (name, (imports, (keywords, errors)))) =
                             pair string (pair string (pair (list string)
                               (pair (list (pair string (pair string (list string))))
                                 (list YXML.string_of_body)))) a;
                           val imports' = map (rpair Position.none) imports;
                           val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
                           val header = Thy_Header.make (name, Position.none) imports' keywords';
                         in Document.Deps {master = master, header = header, errors = errors} end,
                       fn (a :: b, c) =>
                         Document.Perspective (bool_atom a, map int_atom b,
                           list (pair int (pair string (list string))) c)])
                 end);
 
             val _ = Execution.discontinue ();
 
             val (edited, removed, assign_update, state') =
               Document.update old_id new_id edits consolidate state;
             val _ =
               (singleton o Future.forks)
                {name = "Document.update/remove", group = NONE,
                 deps = Execution.snapshot removed,
                 pri = Task_Queue.urgent_pri + 2, interrupts = false}
                (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
 
             val _ =
               Output.protocol_message Markup.assign_update
-                ((new_id, edited, assign_update) |>
+                [(new_id, edited, assign_update) |>
                   let
                     open XML.Encode;
                     fun encode_upd (a, bs) =
                       string (space_implode "," (map Value.print_int (a :: bs)));
-                  in triple int (list string) (list encode_upd) end);
+                  in triple int (list string) (list encode_upd) end];
           in Document.start_execution state' end)));
 
 val _ =
   Protocol_Command.define "Document.remove_versions"
     (fn [versions_yxml] => Document.change_state (fn state =>
       let
         val versions =
           YXML.parse_body versions_yxml |>
             let open XML.Decode in list int end;
         val state1 = Document.remove_versions versions state;
-        val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)];
+        val _ = Output.protocol_message Markup.removed_versions [[XML.Text (versions_yxml)]];
       in state1 end));
 
 val _ =
   Protocol_Command.define "Document.dialog_result"
     (fn [serial, result] =>
       Active.dialog_result (Value.parse_int serial) result
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
 
 val _ =
   Protocol_Command.define "ML_Heap.full_gc"
     (fn [] => ML_Heap.full_gc ());
 
 val _ =
   Protocol_Command.define "ML_Heap.share_common_data"
     (fn [] => ML_Heap.share_common_data ());
 
 end;
diff --git a/src/Pure/PIDE/prover.scala b/src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala
+++ b/src/Pure/PIDE/prover.scala
@@ -1,368 +1,326 @@
 /*  Title:      Pure/PIDE/prover.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Prover process wrapping.
 */
 
 package isabelle
 
 
 import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
 
 
 object Prover
 {
   /* messages */
 
   sealed abstract class Message
   type Receiver = Message => Unit
 
   class Input(val name: String, val args: List[String]) extends Message
   {
     override def toString: String =
       XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
         args.flatMap(s =>
           List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString
   }
 
   class Output(val message: XML.Elem) extends Message
   {
     def kind: String = message.markup.name
     def properties: Properties.T = message.markup.properties
     def body: XML.Body = message.body
 
     def is_init: Boolean = kind == Markup.INIT
     def is_exit: Boolean = kind == Markup.EXIT
     def is_stdout: Boolean = kind == Markup.STDOUT
     def is_stderr: Boolean = kind == Markup.STDERR
     def is_system: Boolean = kind == Markup.SYSTEM
     def is_status: Boolean = kind == Markup.STATUS
     def is_report: Boolean = kind == Markup.REPORT
     def is_syslog: Boolean = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
       val res =
         if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body, metric = Symbol.Metric)
       if (properties.isEmpty)
-        kind.toString + " [[" + res + "]]"
+        kind + " [[" + res + "]]"
       else
-        kind.toString + " " +
+        kind + " " +
           (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
     }
   }
 
-  class Protocol_Output(props: Properties.T, val bytes: Bytes)
+  class Protocol_Error(msg: String) extends Exception(msg)
+  def bad_header(print: String): Nothing = throw new Protocol_Error("bad message header: " + print)
+  def bad_chunks(): Nothing = throw new Protocol_Error("bad message chunks")
+
+  def the_chunk(chunks: List[Bytes], print: => String): Bytes =
+    chunks match {
+      case List(chunk) => chunk
+      case _ => throw new Protocol_Error("single chunk expected: " + print)
+    }
+
+  class Protocol_Output(props: Properties.T, val chunks: List[Bytes])
     extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
   {
-    lazy val text: String = bytes.text
+    def chunk: Bytes = the_chunk(chunks, toString)
+    lazy val text: String = chunk.text
   }
 }
 
 
 class Prover(
   receiver: Prover.Receiver,
   cache: XML.Cache,
   channel: System_Channel,
   process: Bash.Process) extends Protocol
 {
   /** receiver output **/
 
   private def system_output(text: String): Unit =
   {
     receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
-  private def protocol_output(props: Properties.T, bytes: Bytes): Unit =
+  private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit =
   {
-    receiver(new Prover.Protocol_Output(cache.props(props), bytes))
+    receiver(new Prover.Protocol_Output(cache.props(props), chunks))
   }
 
   private def output(kind: String, props: Properties.T, body: XML.Body): Unit =
   {
     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
     val reports = Protocol_Message.reports(props, body)
     for (msg <- main :: reports) receiver(new Prover.Output(cache.elem(msg)))
   }
 
   private def exit_message(result: Process_Result): Unit =
   {
     output(Markup.EXIT, Markup.Process_Result(result),
       List(XML.Text(result.print_return_code)))
   }
 
 
 
   /** process manager **/
 
   private val process_result: Future[Process_Result] =
     Future.thread("process_result") {
       val rc = process.join
       val timing = process.get_timing
       Process_Result(rc, timing = timing)
     }
 
   private def terminate_process(): Unit =
   {
     try { process.terminate() }
     catch {
       case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
     }
   }
 
   private val process_manager = Isabelle_Thread.fork(name = "process_manager")
   {
     val stdout = physical_output(false)
 
     val (startup_failed, startup_errors) =
     {
       var finished: Option[Boolean] = None
       val result = new StringBuilder(100)
       while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
         while (finished.isEmpty && process.stderr.ready) {
           try {
             val c = process.stderr.read
             if (c == 2) finished = Some(true)
             else result += c.toChar
           }
           catch { case _: IOException => finished = Some(false) }
         }
         Time.seconds(0.05).sleep
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
     if (startup_errors != "") system_output(startup_errors)
 
     if (startup_failed) {
       terminate_process()
       process_result.join
       stdout.join
       exit_message(Process_Result(127))
     }
     else {
       val (command_stream, message_stream) = channel.rendezvous()
 
       command_input_init(command_stream)
       val stderr = physical_output(true)
       val message = message_output(message_stream)
 
       val result = process_result.join
       system_output("process terminated")
       command_input_close()
       for (thread <- List(stdout, stderr, message)) thread.join
       system_output("process_manager terminated")
       exit_message(result)
     }
     channel.shutdown()
   }
 
 
   /* management methods */
 
   def join(): Unit = process_manager.join()
 
   def terminate(): Unit =
   {
     system_output("Terminating prover process")
     command_input_close()
 
     var count = 10
     while (!process_result.is_finished && count > 0) {
       Time.seconds(0.1).sleep
       count -= 1
     }
     if (!process_result.is_finished) terminate_process()
   }
 
 
 
   /** process streams **/
 
   /* command input */
 
   private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
 
   private def command_input_close(): Unit = command_input.foreach(_.shutdown())
 
   private def command_input_init(raw_stream: OutputStream): Unit =
   {
     val name = "command_input"
     val stream = new BufferedOutputStream(raw_stream)
     command_input =
       Some(
         Consumer_Thread.fork(name)(
           consume =
             {
               case chunks =>
                 try {
                   Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream)
                   chunks.foreach(_.write_stream(stream))
                   stream.flush
                   true
                 }
                 catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
             },
           finish = { case () => stream.close(); system_output(name + " terminated") }
         )
       )
   }
 
 
   /* physical output */
 
   private def physical_output(err: Boolean): Thread =
   {
     val (name, reader, markup) =
       if (err) ("standard_error", process.stderr, Markup.STDERR)
       else ("standard_output", process.stdout, Markup.STDOUT)
 
     Isabelle_Thread.fork(name = name) {
       try {
         var result = new StringBuilder(100)
         var finished = false
         while (!finished) {
           //{{{
           var c = -1
           var done = false
           while (!done && (result.isEmpty || reader.ready)) {
             c = reader.read
             if (c >= 0) result.append(c.asInstanceOf[Char])
             else done = true
           }
           if (result.nonEmpty) {
             output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
             result.clear()
           }
           else {
             reader.close()
             finished = true
           }
           //}}}
         }
       }
       catch { case e: IOException => system_output(name + ": " + e.getMessage) }
       system_output(name + " terminated")
     }
   }
 
 
   /* message output */
 
   private def message_output(stream: InputStream): Thread =
   {
-    class EOF extends Exception
-    class Protocol_Error(msg: String) extends Exception(msg)
-
-    val name = "message_output"
-    Isabelle_Thread.fork(name = name) {
-      val default_buffer = new Array[Byte](65536)
-      var c = -1
+    def decode_chunk(chunk: Bytes): XML.Body = YXML.parse_body_failsafe(chunk.symbols)
 
-      def read_int(): Int =
-      //{{{
-      {
-        var n = 0
-        c = stream.read
-        if (c == -1) throw new EOF
-        while (48 <= c && c <= 57) {
-          n = 10 * n + (c - 48)
-          c = stream.read
-        }
-        if (c != 10)
-          throw new Protocol_Error("malformed header: expected integer followed by newline")
-        else n
-      }
-      //}}}
-
-      def read_chunk_bytes(): (Array[Byte], Int) =
-      //{{{
-      {
-        val n = read_int()
-        val buf =
-          if (n <= default_buffer.length) default_buffer
-          else new Array[Byte](n)
-
-        var i = 0
-        var m = 0
-        do {
-          m = stream.read(buf, i, n - i)
-          if (m != -1) i += m
+    val thread_name = "message_output"
+    Isabelle_Thread.fork(name = thread_name) {
+      try {
+        var finished = false
+        while (!finished) {
+          Byte_Message.read_message(stream) match {
+            case None => finished = true
+            case Some(header :: chunks) =>
+              decode_chunk(header) match {
+                case List(XML.Elem(Markup(name, props), Nil)) =>
+                  val kind = name.intern
+                  if (kind == Markup.PROTOCOL) protocol_output(props, chunks)
+                  else {
+                    val body = decode_chunk(Prover.the_chunk(chunks, name))
+                    output(kind, props, body)
+                  }
+                case _ => Prover.bad_header(header.toString)
+              }
+            case Some(_) => Prover.bad_chunks()
+          }
         }
-        while (m != -1 && n > i)
-
-        if (i != n)
-          throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
-
-        (buf, n)
-      }
-      //}}}
-
-      def read_chunk(): XML.Body =
-      {
-        val (buf, n) = read_chunk_bytes()
-        YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n))
-      }
-
-      try {
-        do {
-          try {
-            val header = read_chunk()
-            header match {
-              case List(XML.Elem(Markup(name, props), Nil)) =>
-                val kind = name.intern
-                if (kind == Markup.PROTOCOL) {
-                  val (buf, n) = read_chunk_bytes()
-                  protocol_output(props, Bytes(buf, 0, n))
-                }
-                else {
-                  val body = read_chunk()
-                  output(kind, props, body)
-                }
-              case _ =>
-                read_chunk()
-                throw new Protocol_Error("bad header: " + header.toString)
-            }
-          }
-          catch { case _: EOF => }
-        }
-        while (c != -1)
       }
       catch {
         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
-        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
+        case e: Prover.Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
       }
       stream.close()
 
-      system_output(name + " terminated")
+      system_output(thread_name + " terminated")
     }
   }
 
 
 
   /** protocol commands **/
 
   var trace: Boolean = false
 
   def protocol_command_raw(name: String, args: List[Bytes]): Unit =
     command_input match {
       case Some(thread) if thread.is_active =>
         if (trace) {
           val payload = args.foldLeft(0) { case (n, b) => n + b.length }
           Output.writeln(
             "protocol_command " + name + ", args = " + args.length + ", payload = " + payload)
         }
         thread.send(Bytes(name) :: args)
       case _ => error("Inactive prover input thread for command " + quote(name))
     }
 
   def protocol_command_args(name: String, args: List[String]): Unit =
   {
     receiver(new Prover.Input(name, args))
     protocol_command_raw(name, args.map(Bytes(_)))
   }
 
   def protocol_command(name: String, args: String*): Unit =
     protocol_command_args(name, args.toList)
 }
diff --git a/src/Pure/PIDE/session.scala b/src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala
+++ b/src/Pure/PIDE/session.scala
@@ -1,774 +1,774 @@
 /*  Title:      Pure/PIDE/session.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 PIDE editor session, potentially with running prover process.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.Queue
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 
 object Session
 {
   /* outlets */
 
   object Consumer
   {
     def apply[A](name: String)(consume: A => Unit): Consumer[A] =
       new Consumer[A](name, consume)
   }
   final class Consumer[-A] private(val name: String, val consume: A => Unit)
 
   class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
   {
     private val consumers = Synchronized[List[Consumer[A]]](Nil)
 
     def += (c: Consumer[A]): Unit = consumers.change(Library.update(c))
     def -= (c: Consumer[A]): Unit = consumers.change(Library.remove(c))
 
     def post(a: A): Unit =
     {
       for (c <- consumers.value.iterator) {
         dispatcher.send(() =>
           try { c.consume(a) }
           catch {
             case exn: Throwable =>
               Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
           })
       }
     }
   }
 
 
   /* change */
 
   sealed case class Change(
     previous: Document.Version,
     syntax_changed: List[Document.Node.Name],
     deps_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
     consolidate: List[Document.Node.Name],
     version: Document.Version)
 
   case object Change_Flush
 
 
   /* events */
 
   //{{{
   case class Command_Timing(props: Properties.T)
   case class Theory_Timing(props: Properties.T)
   case class Runtime_Statistics(props: Properties.T)
   case class Task_Statistics(props: Properties.T)
   case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
   case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
   sealed abstract class Phase
   {
     def print: String =
       this match {
         case Terminated(result) => if (result.ok) "finished" else "failed"
         case _ => Word.lowercase(this.toString)
       }
   }
   case object Inactive extends Phase  // stable
   case object Startup extends Phase  // transient
   case object Ready extends Phase  // metastable
   case object Shutdown extends Phase  // transient
   case class Terminated(result: Process_Result) extends Phase  // stable
   //}}}
 
 
   /* syslog */
 
   private[Session] class Syslog(limit: Int)
   {
     private var queue = Queue.empty[XML.Elem]
     private var length = 0
 
     def += (msg: XML.Elem): Unit = synchronized {
       queue = queue.enqueue(msg)
       length += 1
       if (length > limit) queue = queue.dequeue._2
     }
 
     def content: String = synchronized {
       cat_lines(queue.iterator.map(XML.content)) +
       (if (length > limit) "\n(A total of " + length + " messages...)" else "")
     }
   }
 
 
   /* protocol handlers */
 
   type Protocol_Function = Prover.Protocol_Output => Boolean
 
   abstract class Protocol_Handler extends Isabelle_System.Service
   {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
     def functions: List[(String, Protocol_Function)] = Nil
     def prover_options(options: Options): Options = options
   }
 }
 
 
 class Session(_session_options: => Options, val resources: Resources) extends Document.Session
 {
   session =>
 
   val cache: XML.Cache = XML.Cache.make()
 
   def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
     Command.Blobs_Info.none
 
 
   /* global flags */
 
   @volatile var timing: Boolean = false
   @volatile var verbose: Boolean = false
 
 
   /* dynamic session options */
 
   def session_options: Options = _session_options
 
   def output_delay: Time = session_options.seconds("editor_output_delay")
   def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay")
   def prune_delay: Time = session_options.seconds("editor_prune_delay")
   def prune_size: Int = session_options.int("editor_prune_size")
   def syslog_limit: Int = session_options.int("editor_syslog_limit")
   def reparse_limit: Int = session_options.int("editor_reparse_limit")
 
 
   /* dispatcher */
 
   private val dispatcher =
     Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
 
   def assert_dispatcher[A](body: => A): A =
   {
     assert(dispatcher.check_thread)
     body
   }
 
   def require_dispatcher[A](body: => A): A =
   {
     require(dispatcher.check_thread, "not on dispatcher thread")
     body
   }
 
   def send_dispatcher(body: => Unit): Unit =
   {
     if (dispatcher.check_thread) body
     else dispatcher.send(() => body)
   }
 
   def send_wait_dispatcher(body: => Unit): Unit =
   {
     if (dispatcher.check_thread) body
     else dispatcher.send_wait(() => body)
   }
 
 
   /* outlets */
 
   val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher)
   val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher)
   val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher)
   val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher)
   val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher)
   val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
   val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
   val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher)
   val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher)
   val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
   val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
   val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
   val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
   val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher)
 
   val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck!
 
 
   /** main protocol manager **/
 
   /* internal messages */
 
   private case class Start(start_prover: Prover.Receiver => Prover)
   private case object Stop
   private case class Get_State(promise: Promise[Document.State])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Update_Options(options: Options)
   private case object Consolidate_Execution
   private case object Prune_History
 
 
   /* phase */
 
   private def post_phase(new_phase: Session.Phase): Session.Phase =
   {
     phase_changed.post(new_phase)
     new_phase
   }
   private val _phase = Synchronized[Session.Phase](Session.Inactive)
   private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase))
 
   def phase: Session.Phase = _phase.value
   def is_ready: Boolean = phase == Session.Ready
 
 
   /* syslog */
 
   private val syslog = new Session.Syslog(syslog_limit)
   def syslog_content(): String = syslog.content
 
 
   /* pipelined change parsing */
 
   private case class Text_Edits(
     previous: Future[Document.Version],
     doc_blobs: Document.Blobs,
     text_edits: List[Document.Edit_Text],
     consolidate: List[Document.Node.Name],
     version_result: Promise[Document.Version])
 
   private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
   {
     case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
       val prev = previous.get_finished
       val change =
         Timing.timeit("parse_change", timing) {
           resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
         }
       version_result.fulfill(change.version)
       manager.send(change)
       true
   }
 
 
   /* buffered changes */
 
   private object change_buffer
   {
     private var assignment: Boolean = false
     private var nodes: Set[Document.Node.Name] = Set.empty
     private var commands: Set[Command] = Set.empty
 
     def flush(): Unit = synchronized {
       if (assignment || nodes.nonEmpty || commands.nonEmpty)
         commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
       if (nodes.nonEmpty) consolidation.update(nodes)
       assignment = false
       nodes = Set.empty
       commands = Set.empty
     }
     private val delay_flush = Delay.first(output_delay) { flush() }
 
     def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
       synchronized {
         assignment |= assign
         for (node <- edited_nodes) {
           nodes += node
         }
         for (command <- cmds) {
           nodes += command.node_name
           command.blobs_names.foreach(nodes += _)
           commands += command
         }
         delay_flush.invoke()
       }
 
     def shutdown(): Unit =
     {
       delay_flush.revoke()
       flush()
     }
   }
 
 
   /* postponed changes */
 
   private object postponed_changes
   {
     private var postponed: List[Session.Change] = Nil
 
     def store(change: Session.Change): Unit = synchronized { postponed ::= change }
 
     def flush(state: Document.State): List[Session.Change] = synchronized {
       val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
       postponed = unassigned
       assigned.reverse
     }
   }
 
 
   /* node consolidation */
 
   private object consolidation
   {
     private val delay =
       Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) }
 
     private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
     private val state = Synchronized(init_state)
 
     def exit(): Unit =
     {
       delay.revoke()
       state.change(_ => None)
     }
 
     def update(new_nodes: Set[Document.Node.Name] = Set.empty): Unit =
     {
       val active =
         state.change_result(st =>
           (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)))
       if (active) delay.invoke()
     }
 
     def flush(): Set[Document.Node.Name] =
       state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None))
   }
 
 
   /* prover process */
 
   private object prover
   {
     private val variable = Synchronized[Option[Prover]](None)
 
     def defined: Boolean = variable.value.isDefined
     def get: Prover = variable.value.get
     def set(p: Prover): Unit = variable.change(_ => Some(p))
     def reset: Unit = variable.change(_ => None)
     def await_reset(): Unit = variable.guarded_access({ case None => Some((), None) case _ => None })
   }
 
 
   /* file formats and protocol handlers */
 
   private lazy val file_formats: File_Format.Session =
     File_Format.registry.start_session(session)
 
   private val protocol_handlers = Protocol_Handlers.init(session)
 
   def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] =
     protocol_handlers.get(c.getName) match {
       case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C])
       case _ => None
     }
 
   def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
     protocol_handlers.init(handler)
 
   def prover_options(options: Options): Options =
     protocol_handlers.prover_options(file_formats.prover_options(options))
 
 
   /* debugger */
 
   private val debugger_handler = new Debugger.Handler(this)
   init_protocol_handler(debugger_handler)
 
   def debugger: Debugger = debugger_handler.debugger
 
 
   /* manager thread */
 
   private val delay_prune =
     Delay.first(prune_delay) { manager.send(Prune_History) }
 
   private val manager: Consumer_Thread[Any] =
   {
     /* global state */
     val global_state = Synchronized(Document.State.init)
 
 
     /* raw edits */
 
     def handle_raw_edits(
       doc_blobs: Document.Blobs = Document.Blobs.empty,
       edits: List[Document.Edit_Text] = Nil,
       consolidate: List[Document.Node.Name] = Nil): Unit =
     //{{{
     {
       require(prover.defined, "prover process not defined (handle_raw_edits)")
 
       if (edits.nonEmpty) prover.get.discontinue_execution()
 
       val previous = global_state.value.history.tip.version
       val version = Future.promise[Document.Version]
       global_state.change(_.continue_history(previous, edits, version))
 
       raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
       change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version))
     }
     //}}}
 
 
     /* resulting changes */
 
     def handle_change(change: Session.Change): Unit =
     //{{{
     {
       require(prover.defined, "prover process not defined (handle_change)")
 
       // define commands
       {
         val id_commands = new mutable.ListBuffer[Command]
         def id_command(command: Command): Unit =
         {
           for {
             (name, digest) <- command.blobs_defined
             if !global_state.value.defined_blob(digest)
           } {
             change.version.nodes(name).get_blob match {
               case Some(blob) =>
                 global_state.change(_.define_blob(digest))
                 prover.get.define_blob(digest, blob.bytes)
               case None =>
                 Output.error_message("Missing blob " + quote(name.toString))
             }
           }
 
           if (!global_state.value.defined_command(command.id)) {
             global_state.change(_.define_command(command))
             id_commands += command
           }
         }
         for { (_, edit) <- change.doc_edits } {
           edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) })
         }
         if (id_commands.nonEmpty) {
           prover.get.define_commands_bulk(resources, id_commands.toList)
         }
       }
 
       val assignment = global_state.value.the_assignment(change.previous).check_finished
       global_state.change(_.define_version(change.version, assignment))
 
       prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
       resources.commit(change)
     }
     //}}}
 
 
     /* prover output */
 
     def handle_output(output: Prover.Output): Unit =
     //{{{
     {
       def bad_output(): Unit =
       {
         if (verbose)
           Output.warning("Ignoring bad prover output: " + output.message.toString)
       }
 
       def change_command(f: Document.State => (Command.State, Document.State)): Unit =
       {
         try {
           val st = global_state.change_result(f)
           if (!st.command.span.is_theory) {
             change_buffer.invoke(false, Nil, List(st.command))
           }
         }
         catch { case _: Document.State.Fail => bad_output() }
       }
 
       output match {
         case msg: Prover.Protocol_Output =>
           val handled = protocol_handlers.invoke(msg)
           if (!handled) {
             msg.properties match {
               case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
                 command_timings.post(Session.Command_Timing(props))
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
                 change_command(_.accumulate(state_id, cache.elem(message), cache))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))
 
               case Markup.Task_Statistics(props) =>
                 task_statistics.post(Session.Task_Statistics(props))
 
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 val id = Value.Long.unapply(args.id.get).get
-                val export = Export.make_entry("", args, msg.bytes, cache)
+                val export = Export.make_entry("", args, msg.chunk, cache)
                 change_command(_.add_export(id, (args.serial, export)))
 
               case Protocol.Loading_Theory(node_name, id) =>
                 val blobs_info = build_blobs_info(node_name)
                 try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) }
                 catch { case _: Document.State.Fail => bad_output() }
 
               case List(Markup.Commands_Accepted.PROPERTY) =>
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
                     ids.foreach(id =>
                       change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache)))
                   case _ => bad_output()
                 }
 
               case List(Markup.Assign_Update.PROPERTY) =>
                 msg.text match {
                   case Protocol.Assign_Update(id, edited, update) =>
                     try {
                       val (edited_nodes, cmds) =
                         global_state.change_result(_.assign(id, edited, update))
                       change_buffer.invoke(true, edited_nodes, cmds)
                       manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
                   case _ => bad_output()
                 }
                 delay_prune.invoke()
 
               case List(Markup.Removed_Versions.PROPERTY) =>
                 msg.text match {
                   case Protocol.Removed(removed) =>
                     try {
                       global_state.change(_.removed_versions(removed))
                       manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
                   case _ => bad_output()
                 }
 
               case _ => bad_output()
             }
           }
         case _ =>
           output.properties match {
             case Position.Id(state_id) =>
               change_command(_.accumulate(state_id, output.message, cache))
 
             case _ if output.is_init =>
               val init_ok =
                 try {
                   Isabelle_System.make_services(classOf[Session.Protocol_Handler])
                     .foreach(init_protocol_handler)
                   true
                 }
                 catch {
                   case exn: Throwable =>
                     prover.get.protocol_command("Prover.stop", "1", Exn.message(exn))
                     false
                 }
 
               if (init_ok) {
                 prover.get.options(prover_options(session_options))
                 prover.get.init_session(resources)
 
                 phase = Session.Ready
                 debugger.ready()
               }
 
             case Markup.Process_Result(result) if output.is_exit =>
               if (prover.defined) protocol_handlers.exit()
               for (id <- global_state.value.theories.keys) {
                 val snapshot = global_state.change_result(_.end_theory(id))
                 finished_theories.post(snapshot)
               }
               file_formats.stop_session
               phase = Session.Terminated(result)
               prover.reset
 
             case _ =>
               raw_output_messages.post(output)
           }
         }
     }
     //}}}
 
 
     /* main thread */
 
     Consumer_Thread.fork[Any]("Session.manager", daemon = true)
     {
       case arg: Any =>
         //{{{
         arg match {
           case output: Prover.Output =>
             if (output.is_syslog) {
               syslog += output.message
               syslog_messages.post(output)
             }
 
             if (output.is_stdout || output.is_stderr)
               raw_output_messages.post(output)
             else handle_output(output)
 
             all_messages.post(output)
 
           case input: Prover.Input =>
             all_messages.post(input)
 
           case Start(start_prover) if !prover.defined =>
             prover.set(start_prover(manager.send(_)))
 
           case Stop =>
             consolidation.exit()
             delay_prune.revoke()
             if (prover.defined) {
               global_state.change(_ => Document.State.init)
               prover.get.terminate()
             }
 
           case Get_State(promise) =>
             promise.fulfill(global_state.value)
 
           case Consolidate_Execution =>
             if (prover.defined) {
               val state = global_state.value
               state.stable_tip_version match {
                 case None => consolidation.update()
                 case Some(version) =>
                   val consolidate =
                     consolidation.flush().iterator.filter(name =>
                       !resources.session_base.loaded_theory(name) &&
                       !state.node_consolidated(version, name) &&
                       state.node_maybe_consolidated(version, name)).toList
                   if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate)
               }
             }
 
           case Prune_History =>
             if (prover.defined) {
               val old_versions = global_state.change_result(_.remove_versions(prune_size))
               if (old_versions.nonEmpty) prover.get.remove_versions(old_versions)
             }
 
           case Update_Options(options) =>
             if (prover.defined && is_ready) {
               prover.get.options(prover_options(options))
               handle_raw_edits()
             }
             global_options.post(Session.Global_Options(options))
 
           case Cancel_Exec(exec_id) if prover.defined =>
             prover.get.cancel_exec(exec_id)
 
           case Session.Raw_Edits(doc_blobs, edits) if prover.defined =>
             handle_raw_edits(doc_blobs = doc_blobs, edits = edits)
 
           case Session.Dialog_Result(id, serial, result) if prover.defined =>
             prover.get.dialog_result(serial, result)
             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
 
           case Protocol_Command(name, args) if prover.defined =>
             prover.get.protocol_command_args(name, args)
 
           case change: Session.Change if prover.defined =>
             val state = global_state.value
             if (!state.removing_versions && state.is_assigned(change.previous))
               handle_change(change)
             else postponed_changes.store(change)
 
           case Session.Change_Flush if prover.defined =>
             val state = global_state.value
             if (!state.removing_versions)
               postponed_changes.flush(state).foreach(handle_change)
 
           case bad =>
             if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
         }
         true
         //}}}
     }
   }
 
 
   /* main operations */
 
   def get_state(): Document.State =
   {
     if (manager.is_active) {
       val promise = Future.promise[Document.State]
       manager.send_wait(Get_State(promise))
       promise.join
     }
     else Document.State.init
   }
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
     get_state().snapshot(name, pending_edits)
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
     resources.session_base.overall_syntax
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot =
   {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
       output_delay.sleep
       await_stable_snapshot()
     }
     else snapshot
   }
 
   def start(start_prover: Prover.Receiver => Prover): Unit =
   {
     file_formats
     _phase.change(
       {
         case Session.Inactive =>
           manager.send(Start(start_prover))
           post_phase(Session.Startup)
         case phase => error("Cannot start prover in phase " + quote(phase.print))
       })
   }
 
   def stop(): Process_Result =
   {
     val was_ready =
       _phase.guarded_access(
         {
           case Session.Startup | Session.Shutdown => None
           case Session.Terminated(_) => Some((false, phase))
           case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
           case Session.Ready => Some((true, post_phase(Session.Shutdown)))
         })
     if (was_ready) manager.send(Stop)
     prover.await_reset()
 
     change_parser.shutdown()
     change_buffer.shutdown()
     manager.shutdown()
     dispatcher.shutdown()
 
     phase match {
       case Session.Terminated(result) => result
       case phase => error("Bad session phase after shutdown: " + quote(phase.print))
     }
   }
 
   def protocol_command(name: String, args: String*): Unit =
     manager.send(Protocol_Command(name, args.toList))
 
   def cancel_exec(exec_id: Document_ID.Exec): Unit =
     manager.send(Cancel_Exec(exec_id))
 
   def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Unit =
     if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits))
 
   def update_options(options: Options): Unit =
     manager.send_wait(Update_Options(options))
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String): Unit =
     manager.send(Session.Dialog_Result(id, serial, result))
 }
diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML
+++ b/src/Pure/System/isabelle_process.ML
@@ -1,228 +1,228 @@
 (*  Title:      Pure/System/isabelle_process.ML
     Author:     Makarius
 
 Isabelle process wrapper.
 *)
 
 signature ISABELLE_PROCESS =
 sig
   val is_active: unit -> bool
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
   val init_options: unit -> unit
   val init_options_interactive: unit -> unit
   val init: unit -> unit
   val init_build: unit -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
 struct
 
 (* print mode *)
 
 val isabelle_processN = "isabelle_process";
 
 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
 
 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
 
 val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
 
 
 (* restricted tracing messages *)
 
 val tracing_messages =
   Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
 
 fun reset_tracing exec_id =
   Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
 
 fun update_tracing () =
   (case Position.parse_id (Position.thread_data ()) of
     NONE => ()
   | SOME exec_id =>
       let
         val ok =
           Synchronized.change_result tracing_messages (fn tab =>
             let
               val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
               val limit = Options.default_int "editor_tracing_messages";
               val ok = limit <= 0 orelse n <= limit;
             in (ok, Inttab.update (exec_id, n) tab) end);
       in
         if ok then ()
         else
           let
             val (text, promise) = Active.dialog_text ();
             val _ =
               writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
                 text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
             val m = Value.parse_int (Future.join promise)
               handle Fail _ => error "Stopped";
           in
             Synchronized.change tracing_messages
               (Inttab.map_default (exec_id, 0) (fn k => k - m))
           end
       end);
 
 
 (* init protocol -- uninterruptible *)
 
 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
 
 local
 
 fun recover crash =
   (Synchronized.change crashes (cons crash);
     Output.physical_stderr
       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
 
 fun ml_statistics () =
   Output.protocol_message
     (Markup.ML_statistics {pid = ML_Pid.get (), stats_dir = getenv "POLYSTATSDIR"}) [];
 
 in
 
 fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
   let
     val _ = SHA1.test_samples ()
       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
 
     val _ = Output.physical_stderr Symbol.STX;
 
 
     (* streams *)
 
     val (in_stream, out_stream) = Socket_IO.open_streams address;
     val _ = Byte_Message.write_line out_stream password;
 
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
     val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
 
 
     (* messages *)
 
     val msg_channel = Message_Channel.make out_stream;
 
-    fun message name props body =
-      Message_Channel.send msg_channel (Message_Channel.message name props body);
+    fun message name props chunks =
+      Message_Channel.send msg_channel (Message_Channel.message name props chunks);
 
     fun standard_message props name ss =
       if forall (fn s => s = "") ss then ()
       else
         let
           val pos_props =
             if exists Markup.position_property props then props
             else props @ Position.properties_of (Position.thread_data ());
-        in message name pos_props (XML.blob ss) end;
+        in message name pos_props [XML.blob ss] end;
 
     fun report_message ss =
       if Context_Position.pide_reports ()
       then standard_message [] Markup.reportN ss else ();
 
     val serial_props = Markup.serial_properties o serial;
 
     val message_context =
       Unsynchronized.setmp Private_Output.status_fn (standard_message [] Markup.statusN) #>
       Unsynchronized.setmp Private_Output.report_fn report_message #>
       Unsynchronized.setmp Private_Output.result_fn
         (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #>
       Unsynchronized.setmp Private_Output.writeln_fn
         (fn s => standard_message (serial_props ()) Markup.writelnN s) #>
       Unsynchronized.setmp Private_Output.state_fn
         (fn s => standard_message (serial_props ()) Markup.stateN s) #>
       Unsynchronized.setmp Private_Output.information_fn
         (fn s => standard_message (serial_props ()) Markup.informationN s) #>
       Unsynchronized.setmp Private_Output.tracing_fn
         (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #>
       Unsynchronized.setmp Private_Output.warning_fn
         (fn s => standard_message (serial_props ()) Markup.warningN s) #>
       Unsynchronized.setmp Private_Output.legacy_fn
         (fn s => standard_message (serial_props ()) Markup.legacyN s) #>
       Unsynchronized.setmp Private_Output.error_message_fn
         (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #>
       Unsynchronized.setmp Private_Output.system_message_fn
-        (fn ss => message Markup.systemN [] (XML.blob ss)) #>
+        (fn ss => message Markup.systemN [] [XML.blob ss]) #>
       Unsynchronized.setmp Private_Output.protocol_message_fn
-        (fn props => fn body => message Markup.protocolN props body) #>
+        (fn props => fn chunks => message Markup.protocolN props chunks) #>
       Unsynchronized.setmp print_mode
         ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes));
 
 
     (* protocol *)
 
     fun protocol_loop () =
       let
         val _ =
           (case Byte_Message.read_message in_stream of
             NONE => raise Protocol_Command.STOP 0
           | SOME [] => Output.system_message "Isabelle process: no input"
           | SOME (name :: args) => Protocol_Command.run name args)
           handle exn =>
             if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
             else (Runtime.exn_system_message exn handle crash => recover crash);
       in protocol_loop () end;
 
     fun protocol () =
-     (message Markup.initN [] [XML.Text (Session.welcome ())];
+     (message Markup.initN [] [[XML.Text (Session.welcome ())]];
       ml_statistics ();
       protocol_loop ());
 
     val result = Exn.capture (message_context protocol) ();
 
 
     (* shutdown *)
 
     val _ = Future.shutdown ();
     val _ = Execution.reset ();
     val _ = Message_Channel.shutdown msg_channel;
     val _ = BinIO.closeIn in_stream;
     val _ = BinIO.closeOut out_stream;
 
     val _ = Options.reset_default ();
   in
     (case result of
       Exn.Exn (Protocol_Command.STOP rc) => if rc = 0 then () else exit rc
     | _ => Exn.release result)
   end);
 
 end;
 
 
 (* init options *)
 
 fun init_options () =
  (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   let val proofs = Options.default_int "record_proofs"
   in if proofs < 0 then () else Proofterm.proofs := proofs end;
   Printer.show_markup_default := false);
 
 fun init_options_interactive () =
  (init_options ();
   Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
   Printer.show_markup_default := true);
 
 
 (* generic init *)
 
 fun init_modes modes =
   let
     val address = Options.default_string \<^system_option>\<open>system_channel_address\<close>;
     val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>;
   in
     if address <> "" andalso password <> ""
     then init_protocol modes (address, password)
     else init_options ()
   end;
 
 fun init () = init_modes (protocol_modes1, protocol_modes2);
 fun init_build () = init_modes ([], protocol_modes2);
 
 end;
diff --git a/src/Pure/System/message_channel.ML b/src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML
+++ b/src/Pure/System/message_channel.ML
@@ -1,68 +1,66 @@
 (*  Title:      Pure/System/message_channel.ML
     Author:     Makarius
 
 Preferably asynchronous channel for Isabelle messages.
 *)
 
 signature MESSAGE_CHANNEL =
 sig
   type message
-  val message: string -> Properties.T -> XML.body -> message
+  val message: string -> Properties.T -> XML.body list -> message
   type T
   val send: T -> message -> unit
   val shutdown: T -> unit
   val make: BinIO.outstream -> T
 end;
 
 structure Message_Channel: MESSAGE_CHANNEL =
 struct
 
 (* message *)
 
-datatype message = Message of {body: XML.body, flush: bool};
+datatype message = Message of {chunks: XML.body list, flush: bool};
 
-fun chunk body = XML.Text (string_of_int (YXML.body_size body) ^ "\n") :: body;
-
-fun message name raw_props body =
+fun message name raw_props chunks =
   let
     val robust_props = map (apply2 YXML.embed_controls) raw_props;
-    val header = XML.Elem ((name, robust_props), []);
-  in Message {body = chunk [header] @ chunk body, flush = name = Markup.protocolN} end;
+    val header = [XML.Elem ((name, robust_props), [])];
+  in Message {chunks = header :: chunks, flush = name = Markup.protocolN} end;
 
 
 (* channel *)
 
 datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit};
 
 fun send (Message_Channel {send, ...}) = send;
 fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
 
 val flush_timeout = SOME (seconds 0.02);
 
 fun message_output mbox stream =
   let
     fun continue timeout =
       (case Mailbox.receive timeout mbox of
         [] => (Byte_Message.flush stream; continue NONE)
       | msgs => received timeout msgs)
     and received _ (NONE :: _) = Byte_Message.flush stream
-      | received _ (SOME (Message {body, flush}) :: rest) =
+      | received _ (SOME (Message {chunks, flush}) :: rest) =
           let
-            val _ = List.app (Byte_Message.write_yxml stream) body;
+            val _ = Byte_Message.write_message_yxml stream chunks;
             val timeout = if flush then (Byte_Message.flush stream; NONE) else flush_timeout;
           in received timeout rest end
       | received timeout [] = continue timeout;
   in fn () => continue NONE end;
 
 fun make stream =
   let
     val mbox = Mailbox.create ();
     val thread =
       Isabelle_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
         (message_output mbox stream);
     fun send msg = Mailbox.send mbox (SOME msg);
     fun shutdown () =
       (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Isabelle_Thread.join thread);
   in Message_Channel {send = send, shutdown = shutdown} end;
 
 end;
diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML
+++ b/src/Pure/System/scala.ML
@@ -1,66 +1,66 @@
 (*  Title:      Pure/System/scala.ML
     Author:     Makarius
 
 Invoke Scala functions from the ML runtime.
 *)
 
 signature SCALA =
 sig
   exception Null
   val function: string -> string -> string
 end;
 
 structure Scala: SCALA =
 struct
 
 exception Null;
 
 local
 
 val new_id = string_of_int o Counter.make ();
 
 val results =
   Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table);
 
 val _ =
   Protocol_Command.define "Scala.result"
     (fn [id, tag, res] =>
       let
         val result =
           (case tag of
             "0" => Exn.Exn Null
           | "1" => Exn.Res res
           | "2" => Exn.Exn (ERROR res)
           | "3" => Exn.Exn (Fail res)
           | "4" => Exn.Exn Exn.Interrupt
           | _ => raise Fail ("Bad tag: " ^ tag));
       in Synchronized.change results (Symtab.map_entry id (K result)) end);
 
 in
 
 fun function name arg =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val id = new_id ();
       fun invoke () =
        (Synchronized.change results (Symtab.update (id, Exn.Exn Match));
-        Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]);
+        Output.protocol_message (Markup.invoke_scala name id) [[XML.Text arg]]);
       fun cancel () =
        (Synchronized.change results (Symtab.delete_safe id);
         Output.protocol_message (Markup.cancel_scala id) []);
       fun await_result () =
         Synchronized.guarded_access results
           (fn tab =>
             (case Symtab.lookup tab id of
               SOME (Exn.Exn Match) => NONE
             | SOME result => SOME (result, Symtab.delete id tab)
             | NONE => SOME (Exn.Exn Exn.Interrupt, tab)));
     in
       invoke ();
       Exn.release (restore_attributes await_result ())
         handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
     end) ();
 
 end;
 
 end;
diff --git a/src/Pure/Thy/export.ML b/src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML
+++ b/src/Pure/Thy/export.ML
@@ -1,73 +1,73 @@
 (*  Title:      Pure/Thy/export.ML
     Author:     Makarius
 
 Manage theory exports: compressed blobs.
 *)
 
 signature EXPORT =
 sig
   val report_export: theory -> Path.binding -> unit
   type params =
     {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
   val export_params: params -> XML.body -> unit
   val export: theory -> Path.binding -> XML.body -> unit
   val export_executable: theory -> Path.binding -> XML.body -> unit
   val export_file: theory -> Path.binding -> Path.T -> unit
   val export_executable_file: theory -> Path.binding -> Path.T -> unit
   val markup: theory -> Path.T -> Markup.T
   val message: theory -> Path.T -> string
 end;
 
 structure Export: EXPORT =
 struct
 
 (* export *)
 
 fun report_export thy binding =
   let
     val theory_name = Context.theory_long_name thy;
     val (path, pos) = Path.dest_binding binding;
     val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
   in Context_Position.report_generic (Context.Theory thy) pos markup end;
 
 type params =
   {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
 
 fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
  (report_export thy binding;
   (Output.try_protocol_message o Markup.export)
    {id = Position.get_id (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name thy,
     name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
     compress = compress,
-    strict = strict} body);
+    strict = strict} [body]);
 
 fun export thy binding body =
   export_params
     {theory = thy, binding = binding, executable = false, compress = true, strict = true} body;
 
 fun export_executable thy binding body =
   export_params
     {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
 
 fun export_file thy binding file =
   export thy binding [XML.Text (File.read file)];
 
 fun export_executable_file thy binding file =
   export_executable thy binding [XML.Text (File.read file)];
 
 
 (* information message *)
 
 fun markup thy path =
   let
     val thy_path = Path.basic (Context.theory_long_name thy) + path;
     val name = (Markup.nameN, Path.implode thy_path);
   in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;
 
 fun message thy path =
   "See " ^ Markup.markup (markup thy path) "theory exports";
 
 end;
diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML
+++ b/src/Pure/Thy/thy_info.ML
@@ -1,474 +1,474 @@
 (*  Title:      Pure/Thy/thy_info.ML
     Author:     Makarius
 
 Global theory info database, with auto-loading according to theory and
 file dependencies, and presentation of theory documents.
 *)
 
 signature THY_INFO =
 sig
   type presentation_context =
     {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
       segments: Thy_Output.segment list}
   val adjust_pos_properties: presentation_context -> Position.T -> Properties.T
   val apply_presentation: presentation_context -> theory -> unit
   val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories: Options.T -> string -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
 
 structure Thy_Info: THY_INFO =
 struct
 
 (** theory presentation **)
 
 (* artefact names *)
 
 fun document_name ext thy =
   Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext);
 
 val document_tex_name = document_name "tex";
 
 
 (* hook for consolidated theory *)
 
 type presentation_context =
   {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
     segments: Thy_Output.segment list};
 
 fun adjust_pos_properties (context: presentation_context) pos =
   Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos;
 
 structure Presentation = Theory_Data
 (
   type T = ((presentation_context -> theory -> unit) * stamp) list;
   val empty = [];
   val extend = I;
   fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
 fun apply_presentation (context: presentation_context) thy =
   ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
 val _ =
   Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
         val body = Thy_Output.present_thy options thy segments;
       in
         if Options.string options "document" = "false" then ()
         else
           let
             val thy_name = Context.theory_name thy;
             val document_tex_name = document_tex_name thy;
 
             val latex = Latex.isabelle_body thy_name body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
           in Export.export thy document_tex_name (XML.blob output) end
       end));
 
 
 
 (** thy database **)
 
 (* messages *)
 
 val show_path = space_implode " via " o map quote;
 
 fun cycle_msg names = "Cyclic dependency of " ^ show_path names;
 
 
 (* derived graph operations *)
 
 fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
   handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
 
 fun new_entry name parents entry =
   String_Graph.new_node (name, entry) #> add_deps name parents;
 
 
 (* global thys *)
 
 type deps =
  {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
   imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
 fun master_dir_deps (d: deps option) =
   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 
 local
   val global_thys =
     Synchronized.var "Thy_Info.thys"
       (String_Graph.empty: (deps option * theory option) String_Graph.T);
 in
   fun get_thys () = Synchronized.value global_thys;
   fun change_thys f = Synchronized.change global_thys f;
 end;
 
 fun get_names () = String_Graph.topological_order (get_thys ());
 
 
 (* access thy *)
 
 fun lookup thys name = try (String_Graph.get_node thys) name;
 fun lookup_thy name = lookup (get_thys ()) name;
 
 fun get thys name =
   (case lookup thys name of
     SOME thy => thy
   | NONE => error ("Theory loader: nothing known about theory " ^ quote name));
 
 fun get_thy name = get (get_thys ()) name;
 
 
 (* access deps *)
 
 val lookup_deps = Option.map #1 o lookup_thy;
 
 val master_directory = master_dir_deps o #1 o get_thy;
 
 
 (* access theory *)
 
 fun lookup_theory name =
   (case lookup_thy name of
     SOME (_, SOME theory) => SOME theory
   | _ => NONE);
 
 fun get_theory name =
   (case lookup_theory name of
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
 val get_imports = Resources.imports_of o get_theory;
 
 
 
 (** thy operations **)
 
 (* remove *)
 
 fun remove name thys =
   (case lookup thys name of
     NONE => thys
   | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name)
   | SOME _ =>
       let
         val succs = String_Graph.all_succs thys [name];
         val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
       in fold String_Graph.del_node succs thys end);
 
 val remove_thy = change_thys o remove;
 
 
 (* update *)
 
 fun update deps theory thys =
   let
     val name = Context.theory_long_name theory;
     val parents = map Context.theory_long_name (Theory.parents_of theory);
 
     val thys' = remove name thys;
     val _ = map (get thys') parents;
   in new_entry name parents (SOME deps, SOME theory) thys' end;
 
 fun update_thy deps theory = change_thys (update deps theory);
 
 
 (* scheduling loader tasks *)
 
 datatype result =
   Result of {theory: theory, exec_id: Document_ID.exec,
     present: unit -> unit, commit: unit -> unit, weight: int};
 
 fun theory_result theory =
   Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_present (Result {present, ...}) = present;
 fun result_commit (Result {commit, ...}) = commit;
 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
 
 fun join_theory (Result {theory, exec_id, ...}) =
   let
     val _ = Execution.join [exec_id];
     val res = Exn.capture Thm.consolidate_theory theory;
     val exns = maps Task_Queue.group_status (Execution.peek exec_id);
   in res :: map Exn.Exn exns end;
 
 datatype task =
   Task of string list * (theory list -> result) |
   Finished of theory;
 
 fun task_finished (Task _) = false
   | task_finished (Finished _) = true;
 
 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
 
 val schedule_seq =
   String_Graph.schedule (fn deps => fn (_, task) =>
     (case task of
       Task (parents, body) =>
         let
           val result = body (task_parents deps parents);
           val _ = Par_Exn.release_all (join_theory result);
           val _ = result_present result ();
           val _ = result_commit result ();
         in result_theory result end
     | Finished thy => thy)) #> ignore;
 
 val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
   let
     val futures = tasks
       |> String_Graph.schedule (fn deps => fn (name, task) =>
         (case task of
           Task (parents, body) =>
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = NONE,
                 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
               (fn () =>
                 (case filter (not o can Future.join o #2) deps of
                   [] => body (map (result_theory o Future.join) (task_parents deps parents))
                 | bad =>
                     error
                       ("Failed to load theory " ^ quote name ^
                         " (unresolved " ^ commas_quote (map #1 bad) ^ ")")))
         | Finished theory => Future.value (theory_result theory)));
 
     val results1 = futures
       |> maps (fn future =>
           (case Future.join_result future of
             Exn.Res result => join_theory result
           | Exn.Exn exn => [Exn.Exn exn]));
 
     val results2 = futures
       |> map_filter (Exn.get_res o Future.join_result)
       |> sort result_ord
       |> Par_List.map (fn result => Exn.capture (result_present result) ());
 
     (* FIXME more precise commit order (!?) *)
     val results3 = futures
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
 
     (* FIXME avoid global Execution.reset (!??) *)
     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in () end);
 
 
 (* eval theory *)
 
 fun eval_thy options master_dir header text_pos text parents =
   let
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
 
     val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
     val elements = Thy_Element.parse_elements keywords spans;
 
     val text_id = Position.copy_id text_pos Position.none;
 
     fun init () = Resources.begin_theory master_dir header parents;
 
     fun excursion () =
       let
         fun element_result span_elem (st, _) =
           let
             fun prepare span =
               let
                 val tr =
                   Position.setmp_thread_data text_id
                     (fn () => Command.read_span keywords st master_dir init span) ();
               in Toplevel.timing (Resources.last_timing tr) tr end;
             val elem = Thy_Element.map_element prepare span_elem;
             val (results, st') = Toplevel.element_result keywords elem st;
             val pos' = Toplevel.pos_of (Thy_Element.last_element elem);
           in (results, (st', pos')) end;
 
         val (results, (end_state, end_pos)) =
           fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
 
         val thy = Toplevel.end_theory end_pos end_state;
       in (results, thy) end;
 
     val (results, thy) = cond_timeit true ("theory " ^ quote name) excursion;
 
     fun present () =
       let
         val segments = (spans ~~ maps Toplevel.join_results results)
           |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
         val context: presentation_context =
           {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
       in apply_presentation context thy end;
 
   in (thy, present, size text) end;
 
 
 (* require_thy -- checking database entries wrt. the file-system *)
 
 local
 
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
 fun load_thy options initiators deps text (name, header_pos) keywords parents =
   let
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
 
     val exec_id = Document_ID.make ();
     val id = Document_ID.print exec_id;
     val put_id = Position.put_id id;
     val _ =
       Execution.running Document_ID.none exec_id [] orelse
         raise Fail ("Failed to register execution: " ^ id);
 
     val text_pos = put_id (Path.position thy_path);
     val text_props = Position.properties_of text_pos;
 
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) (XML.blob [text]);
+    val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]];
 
     val _ =
       Position.setmp_thread_data (Position.id_only id) (fn () =>
         (parents, map #2 imports) |> ListPair.app (fn (thy, pos) =>
           Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) ();
 
     val timing_start = Timing.start ();
 
     val header = Thy_Header.make (name, put_id header_pos) imports keywords;
     val (theory, present, weight) =
       eval_thy options dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
     val timing_result = Timing.result timing_start;
     val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
-    val _  = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
+    val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
 
     fun commit () = update_thy deps theory;
   in
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   end;
 
 fun check_thy_deps dir name =
   (case lookup_deps name of
     SOME NONE => (true, NONE, Position.none, get_imports name, [])
   | NONE =>
       let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
       in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   | SOME (SOME {master, ...}) =>
       let
         val {master = master', text = text', theory_pos = theory_pos', imports = imports',
           keywords = keywords'} = Resources.check_thy dir name;
         val deps' = SOME (make_deps master' imports', text');
         val current =
           #2 master = #2 master' andalso
             (case lookup_theory name of
               NONE => false
             | SOME theory => Resources.loaded_files_current theory);
       in (current, deps', theory_pos', imports', keywords') end);
 
 in
 
 fun require_thys options initiators qualifier dir strs tasks =
       fold_map (require_thy options initiators qualifier dir) strs tasks |>> forall I
 and require_thy options initiators qualifier dir (s, require_pos) tasks =
   let
     val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
   in
     (case try (String_Graph.get_node tasks) theory_name of
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
 
           val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name
             handle ERROR msg =>
               cat_error msg
                 ("The error(s) above occurred for theory " ^ quote theory_name ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
           val qualifier' = Resources.theory_qualifier theory_name;
           val dir' = dir + master_dir_deps (Option.map #1 deps);
 
           val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
           val (parents_current, tasks') =
             require_thys options (theory_name :: initiators) qualifier' dir' imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
             if all_current then Finished (get_theory theory_name)
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
               | SOME (dep, text) =>
                   Task (parents,
                     load_thy options initiators dep text (theory_name, theory_pos) keywords));
 
           val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
   end;
 
 end;
 
 
 (* use theories *)
 
 fun use_theories options qualifier imports =
   let val (_, tasks) = require_thys options [] qualifier Path.current imports String_Graph.empty
   in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
   use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)];
 
 
 (* toplevel scripting -- without maintaining database *)
 
 fun script_thy pos txt thy =
   let
     val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
     val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
   in Toplevel.end_theory end_pos end_state end;
 
 
 (* register theory *)
 
 fun register_thy theory =
   let
     val name = Context.theory_long_name theory;
     val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
     val imports = Resources.imports_of theory;
   in
     change_thys (fn thys =>
       let
         val thys' = remove name thys;
         val _ = writeln ("Registering theory " ^ quote name);
       in update (make_deps master imports) theory thys' end)
   end;
 
 
 (* finish all theories *)
 
 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
 
 end;
 
 fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);
diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML
+++ b/src/Pure/Tools/build.ML
@@ -1,98 +1,99 @@
 (*  Title:      Pure/Tools/build.ML
     Author:     Makarius
 
 Build Isabelle sessions.
 *)
 
 structure Build: sig end =
 struct
 
 (* session timing *)
 
 fun session_timing f x =
   let
     val start = Timing.start ();
     val y = f x;
     val timing = Timing.result start;
 
     val threads = string_of_int (Multithreading.max_threads ());
     val props = [("threads", threads)] @ Markup.timing_properties timing;
     val _ = Output.protocol_message (Markup.session_timing :: props) [];
   in y end;
 
 
 (* build theories *)
 
 fun build_theories qualifier (options, thys) =
   let
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
   in
     if null conds then
       (Options.set_default options;
         Isabelle_Process.init_options ();
         Future.fork I;
         (Thy_Info.use_theories options qualifier
         |>
           (case Options.string options "profiling" of
             "" => I
           | "time" => profile_time
           | "allocations" => profile_allocations
           | bad => error ("Bad profiling option: " ^ quote bad))
         |> Unsynchronized.setmp print_mode
             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
     else
       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
         " (undefined " ^ commas conds ^ ")\n")
   end;
 
 
 (* build session *)
 
 val _ =
   Protocol_Command.define "build_session"
     (fn [resources_yxml, args_yxml] =>
         let
           val _ = Resources.init_session_yxml resources_yxml;
           val (session_name, theories) =
             YXML.parse_body args_yxml |>
               let
                 open XML.Decode;
                 val position = Position.of_properties o properties;
               in pair string (list (pair Options.decode (list (pair string position)))) end;
 
           val _ = Session.init session_name;
 
           fun build () =
             let
               val res1 =
                 theories |>
                   (List.app (build_theories session_name)
                     |> session_timing
                     |> Exn.capture);
               val res2 = Exn.capture Session.finish ();
 
               val _ = Resources.finish_session_base ();
               val _ = Par_Exn.release_all [res1, res2];
               val _ =
                 if session_name = Context.PureN
                 then Theory.install_pure (Thy_Info.get_theory Context.PureN) else ();
             in () end;
 
           fun exec e =
             if can Theory.get_pure () then
               Isabelle_Thread.fork
                 {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (),
                   interrupts = false} e
               |> ignore
             else e ();
         in
           exec (fn () =>
             (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn =>
               ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
           |> let open XML.Encode in pair int (list string) end
+          |> single
           |> Output.protocol_message Markup.build_session_finished)
         end
       | _ => raise Match);
 
 end;
diff --git a/src/Pure/Tools/build_job.scala b/src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala
+++ b/src/Pure/Tools/build_job.scala
@@ -1,538 +1,538 @@
 /*  Title:      Pure/Tools/build_job.scala
     Author:     Makarius
 
 Build job running prover process, with rudimentary PIDE session.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 
 
 object Build_Job
 {
   /* theory markup/messages from database */
 
   def read_theory(
     db_context: Sessions.Database_Context,
     resources: Resources,
     session: String,
     theory: String,
     unicode_symbols: Boolean = false): Option[Command] =
   {
     def read(name: String): Export.Entry =
       db_context.get_export(List(session), theory, name)
 
     def read_xml(name: String): XML.Body =
       YXML.parse_body(
         Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
         cache = db_context.cache)
 
     (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
       case (Value.Long(id), thy_file :: blobs_files) =>
         val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
 
         val results =
           Command.Results.make(
             for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
               yield i -> elem)
 
         val blobs =
           blobs_files.map(file =>
           {
             val path = Path.explode(file)
             val name = resources.file_node(path)
             val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
             Command.Blob(name, src_path, None)
           })
         val blobs_xml =
           for (i <- (1 to blobs.length).toList)
             yield read_xml(Export.MARKUP + i)
 
         val blobs_info =
           Command.Blobs_Info(
             for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml }
               yield {
                 val text = XML.content(xml)
                 val chunk = Symbol.Text_Chunk(text)
                 val digest = SHA1.digest(Symbol.encode(text))
                 Exn.Res(Command.Blob(name, src_path, Some((digest, chunk))))
               })
 
         val thy_xml = read_xml(Export.MARKUP)
         val thy_source = XML.content(thy_xml)
 
         val markups_index =
           Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob)
         val markups =
           Command.Markups.make(
             for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
             yield index -> Markup_Tree.from_XML(xml))
 
         val command =
           Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
             blobs_info = blobs_info, results = results, markups = markups)
         Some(command)
       case _ => None
     }
   }
 
 
   /* print messages */
 
   def print_log(
     options: Options,
     session_name: String,
     theories: List[String] = Nil,
     verbose: Boolean = false,
     progress: Progress = new Progress,
     margin: Double = Pretty.default_margin,
     breakgain: Double = Pretty.default_breakgain,
     metric: Pretty.Metric = Symbol.Metric,
     unicode_symbols: Boolean = false): Unit =
   {
     val store = Sessions.store(options)
 
     val resources = Resources.empty
     val session = new Session(options, resources)
 
     using(store.open_database_context())(db_context =>
     {
       val result =
         db_context.input_database(session_name)((db, _) =>
         {
           val theories = store.read_theories(db, session_name)
           val errors = store.read_errors(db, session_name)
           store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
         })
       result match {
         case None => error("Missing build database for session " + quote(session_name))
         case Some((used_theories, errors, rc)) =>
           val bad_theories = theories.filterNot(used_theories.toSet)
           if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories))
 
           val print_theories =
             if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
           for (thy <- print_theories) {
             val thy_heading = "\nTheory " + quote(thy) + ":"
             read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols)
             match {
               case None => progress.echo(thy_heading + " MISSING")
               case Some(command) =>
                 val snapshot = Document.State.init.snippet(command)
                 val rendering = new Rendering(snapshot, options, session)
                 val messages =
                   rendering.text_messages(Text.Range.full)
                     .filter(message => verbose || Protocol.is_exported(message.info))
                 if (messages.nonEmpty) {
                   val line_document = Line.Document(command.source)
                   progress.echo(thy_heading)
                   for (Text.Info(range, elem) <- messages) {
                     val line = line_document.position(range.start).line1
                     val pos = Position.Line_File(line, command.node_name.node)
                     progress.echo(
                       Protocol.message_text(elem, heading = true, pos = pos,
                         margin = margin, breakgain = breakgain, metric = metric))
                   }
                 }
             }
           }
 
           if (errors.nonEmpty) {
             val msg = Symbol.output(unicode_symbols, cat_lines(errors))
             progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
           }
           if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc))
       }
     })
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("log", "print messages from build database",
     Scala_Project.here, args =>
   {
     /* arguments */
 
     var unicode_symbols = false
     var theories: List[String] = Nil
     var margin = Pretty.default_margin
     var options = Options.init()
     var verbose = false
 
     val getopts = Getopts("""
 Usage: isabelle log [OPTIONS] SESSION
 
   Options are:
     -T NAME      restrict to given theories (multiple options possible)
     -U           output Unicode symbols
     -m MARGIN    margin for pretty printing (default: """ + margin + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           print all messages, including information, tracing etc.
 
   Print messages from the build database of the given session, without any
   checks against current sources: results from a failed build can be
   printed as well.
 """,
       "T:" -> (arg => theories = theories ::: List(arg)),
       "U" -> (_ => unicode_symbols = true),
       "m:" -> (arg => margin = Value.Double.parse(arg)),
       "o:" -> (arg => options = options + arg),
       "v" -> (_ => verbose = true))
 
     val more_args = getopts(args)
     val session_name =
       more_args match {
         case List(session_name) => session_name
         case _ => getopts.usage()
       }
 
     val progress = new Console_Progress()
 
     print_log(options, session_name, theories = theories, verbose = verbose, margin = margin,
       progress = progress, unicode_symbols = unicode_symbols)
   })
 }
 
 class Build_Job(progress: Progress,
   session_name: String,
   val info: Sessions.Info,
   deps: Sessions.Deps,
   store: Sessions.Store,
   do_store: Boolean,
   verbose: Boolean,
   val numa_node: Option[Int],
   command_timings0: List[Properties.T])
 {
   val options: Options = NUMA.policy_options(info.options, numa_node)
 
   private val sessions_structure = deps.sessions_structure
 
   private val future_result: Future[Process_Result] =
     Future.thread("build", uninterruptible = true) {
       val parent = info.parent.getOrElse("")
       val base = deps(parent)
       val result_base = deps(session_name)
 
       val env =
         Isabelle_System.settings() +
           ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
 
       val is_pure = Sessions.is_pure(session_name)
 
       val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
 
       val eval_store =
         if (do_store) {
           (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
           List("ML_Heap.save_child " +
             ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
         }
         else Nil
 
       val resources = new Resources(sessions_structure, base, command_timings = command_timings0)
       val session =
         new Session(options, resources) {
           override val cache: XML.Cache = store.cache
 
           override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
           {
             result_base.load_commands.get(name.expand) match {
               case Some(spans) =>
                 val syntax = result_base.theory_syntax(name)
                 Command.build_blobs_info(syntax, name, spans)
               case None => Command.Blobs_Info.none
             }
           }
         }
 
       object Build_Session_Errors
       {
         private val promise: Promise[List[String]] = Future.promise
 
         def result: Exn.Result[List[String]] = promise.join_result
         def cancel(): Unit = promise.cancel()
         def apply(errs: List[String]): Unit =
         {
           try { promise.fulfill(errs) }
           catch { case _: IllegalStateException => }
         }
       }
 
       val export_consumer =
         Export.consumer(store.open_database(session_name, output = true), store.cache)
 
       val stdout = new StringBuilder(1000)
       val stderr = new StringBuilder(1000)
       val command_timings = new mutable.ListBuffer[Properties.T]
       val theory_timings = new mutable.ListBuffer[Properties.T]
       val session_timings = new mutable.ListBuffer[Properties.T]
       val runtime_statistics = new mutable.ListBuffer[Properties.T]
       val task_statistics = new mutable.ListBuffer[Properties.T]
 
       def fun(
         name: String,
         acc: mutable.ListBuffer[Properties.T],
         unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
       {
         name -> ((msg: Prover.Protocol_Output) =>
           unapply(msg.properties) match {
             case Some(props) => acc += props; true
             case _ => false
           })
       }
 
       session.init_protocol_handler(new Session.Protocol_Handler
         {
           override def exit(): Unit = Build_Session_Errors.cancel()
 
           private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
           {
             val (rc, errors) =
               try {
                 val (rc, errs) =
                 {
                   import XML.Decode._
                   pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
                 }
                 val errors =
                   for (err <- errs) yield {
                     val prt = Protocol_Message.expose_no_reports(err)
                     Pretty.string_of(prt, metric = Symbol.Metric)
                   }
                 (rc, errors)
               }
               catch { case ERROR(err) => (2, List(err)) }
 
             session.protocol_command("Prover.stop", rc.toString)
             Build_Session_Errors(errors)
             true
           }
 
           private def loading_theory(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
               case Markup.Loading_Theory(Markup.Name(name)) =>
                 progress.theory(Progress.Theory(name, session = session_name))
                 false
               case _ => false
             }
 
           private def export(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
               case Protocol.Export(args) =>
-                export_consumer(session_name, args, msg.bytes)
+                export_consumer(session_name, args, msg.chunk)
                 true
               case _ => false
             }
 
           override val functions =
             List(
               Markup.Build_Session_Finished.name -> build_session_finished,
               Markup.Loading_Theory.name -> loading_theory,
               Markup.EXPORT -> export,
               fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
               fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
               fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
         })
 
       session.command_timings += Session.Consumer("command_timings")
         {
           case Session.Command_Timing(props) =>
             for {
               elapsed <- Markup.Elapsed.unapply(props)
               elapsed_time = Time.seconds(elapsed)
               if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
             } command_timings += props.filter(Markup.command_timing_property)
         }
 
       session.runtime_statistics += Session.Consumer("ML_statistics")
         {
           case Session.Runtime_Statistics(props) => runtime_statistics += props
         }
 
       session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories")
         {
           case snapshot =>
             val rendering = new Rendering(snapshot, options, session)
 
             def export(name: String, xml: XML.Body, compress: Boolean = true): Unit =
             {
               val theory_name = snapshot.node_name.theory
               val args =
                 Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress)
               val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml)))
               if (!bytes.is_empty) export_consumer(session_name, args, bytes)
             }
             def export_text(name: String, text: String, compress: Boolean = true): Unit =
               export(name, List(XML.Text(text)), compress = compress)
 
             for (command <- snapshot.snippet_command) {
               export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
             }
 
             export_text(Export.FILES,
               cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false)
 
             for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
               export(Export.MARKUP + (i + 1), xml)
             }
             export(Export.MARKUP, snapshot.xml_markup())
             export(Export.MESSAGES, snapshot.messages.map(_._1))
 
             val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info))
             export_text(Export.CITATIONS, cat_lines(citations))
         }
 
       session.all_messages += Session.Consumer[Any]("build_session_output")
         {
           case msg: Prover.Output =>
             val message = msg.message
             if (msg.is_stdout) {
               stdout ++= Symbol.encode(XML.content(message))
             }
             else if (msg.is_stderr) {
               stderr ++= Symbol.encode(XML.content(message))
             }
             else if (msg.is_exit) {
               val err =
                 "Prover terminated" +
                   (msg.properties match {
                     case Markup.Process_Result(result) => ": " + result.print_rc
                     case _ => ""
                   })
               Build_Session_Errors(List(err))
             }
           case _ =>
         }
 
       val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
       val process =
         Isabelle_Process(session, options, sessions_structure, store,
           logic = parent, raw_ml_system = is_pure,
           use_prelude = use_prelude, eval_main = eval_main,
           cwd = info.dir.file, env = env)
 
       val build_errors =
         Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
           Exn.capture { process.await_startup() } match {
             case Exn.Res(_) =>
               val resources_yxml = resources.init_session_yxml
               val args_yxml =
                 YXML.string_of_body(
                   {
                     import XML.Encode._
                     pair(string, list(pair(Options.encode, list(pair(string, properties)))))(
                       (session_name, info.theories))
                   })
               session.protocol_command("build_session", resources_yxml, args_yxml)
               Build_Session_Errors.result
             case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
           }
         }
 
       val process_result =
         Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() }
 
       session.stop()
 
       val export_errors =
         export_consumer.shutdown(close = true).map(Output.error_message_text)
 
       val (document_output, document_errors) =
         try {
           if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
             using(store.open_database_context())(db_context =>
               {
                 val documents =
                   Presentation.build_documents(session_name, deps, db_context,
                     output_sources = info.document_output,
                     output_pdf = info.document_output,
                     progress = progress,
                     verbose = verbose)
                 db_context.output_database(session_name)(db =>
                   documents.foreach(_.write(db, session_name)))
                 (documents.flatMap(_.log_lines), Nil)
               })
           }
           else (Nil, Nil)
         }
         catch {
           case exn: Presentation.Build_Error => (exn.log_lines, List(exn.message))
           case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
         }
 
       val result =
       {
         val theory_timing =
           theory_timings.iterator.map(
             { case props @ Markup.Name(name) => name -> props }).toMap
         val used_theory_timings =
           for { (name, _) <- deps(session_name).used_theories }
             yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
 
         val more_output =
           Library.trim_line(stdout.toString) ::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
             session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
             document_output
 
         process_result.output(more_output)
           .error(Library.trim_line(stderr.toString))
           .errors_rc(export_errors ::: document_errors)
       }
 
       build_errors match {
         case Exn.Res(build_errs) =>
           val errs = build_errs ::: document_errors
           if (errs.isEmpty) result
           else {
             result.error_rc.output(
               errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
                 errs.map(Protocol.Error_Message_Marker.apply))
           }
         case Exn.Exn(Exn.Interrupt()) =>
           if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
         case Exn.Exn(exn) => throw exn
       }
     }
 
   def terminate(): Unit = future_result.cancel()
   def is_finished: Boolean = future_result.is_finished
 
   private val timeout_request: Option[Event_Timer.Request] =
   {
     if (info.timeout > Time.zero)
       Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
     else None
   }
 
   def join: (Process_Result, Option[String]) =
   {
     val result1 = future_result.join
 
     val was_timeout =
       timeout_request match {
         case None => false
         case Some(request) => !request.cancel()
       }
 
     val result2 =
       if (result1.ok) result1
       else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc
       else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
       else result1
 
     val heap_digest =
       if (result2.ok && do_store && store.output_heap(session_name).is_file)
         Some(Sessions.write_heap_digest(store.output_heap(session_name)))
       else None
 
     (result2, heap_digest)
   }
 }
diff --git a/src/Pure/Tools/debugger.ML b/src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML
+++ b/src/Pure/Tools/debugger.ML
@@ -1,295 +1,295 @@
 (*  Title:      Pure/Tools/debugger.ML
     Author:     Makarius
 
 Interactive debugger for Isabelle/ML.
 *)
 
 signature DEBUGGER =
 sig
   val writeln_message: string -> unit
   val warning_message: string -> unit
   val error_message: string -> unit
 end;
 
 structure Debugger: DEBUGGER =
 struct
 
 (** global state **)
 
 (* output messages *)
 
 fun output_message kind msg =
   if msg = "" then ()
   else
     Output.protocol_message
       (Markup.debugger_output (Isabelle_Thread.get_name ()))
-      [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)];
+      [[XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)]];
 
 val writeln_message = output_message Markup.writelnN;
 val warning_message = output_message Markup.warningN;
 val error_message = output_message Markup.errorN;
 
 fun error_wrapper e = e ()
   handle exn =>
     if Exn.is_interrupt exn then Exn.reraise exn
     else error_message (Runtime.exn_message exn);
 
 
 (* thread input *)
 
 val thread_input =
   Synchronized.var "Debugger.state" (NONE: string list Queue.T Symtab.table option);
 
 fun init_input () = Synchronized.change thread_input (K (SOME Symtab.empty));
 fun exit_input () = Synchronized.change thread_input (K NONE);
 
 fun input thread_name msg =
   if null msg then error "Empty input"
   else
     Synchronized.change thread_input
       (Option.map (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg)));
 
 fun get_input thread_name =
   Synchronized.guarded_access thread_input
     (fn NONE => SOME ([], NONE)
       | SOME input =>
           (case Symtab.lookup input thread_name of
             NONE => NONE
           | SOME queue =>
               let
                 val (msg, queue') = Queue.dequeue queue;
                 val input' =
                   if Queue.is_empty queue' then Symtab.delete_safe thread_name input
                   else Symtab.update (thread_name, queue') input;
               in SOME (msg, SOME input') end));
 
 
 (* global break *)
 
 local
   val break = Synchronized.var "Debugger.break" false;
 in
 
 fun is_break () = Synchronized.value break;
 fun set_break b = Synchronized.change break (K b);
 
 end;
 
 
 
 (** thread state **)
 
 (* stack frame during debugging *)
 
 val debugging_var = Thread_Data.var () : PolyML.DebuggerInterface.debugState list Thread_Data.var;
 
 fun get_debugging () = the_default [] (Thread_Data.get debugging_var);
 val is_debugging = not o null o get_debugging;
 
 fun with_debugging e =
   Thread_Data.setmp debugging_var (SOME (PolyML.DebuggerInterface.debugState (Thread.self ()))) e ();
 
 fun the_debug_state thread_name index =
   (case get_debugging () of
     [] => error ("Missing debugger information for thread " ^ quote thread_name)
   | states =>
       if index < 0 orelse index >= length states then
         error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
           quote thread_name)
       else nth states index);
 
 
 (* flags for single-stepping *)
 
 datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)
 
 val stepping_var = Thread_Data.var () : stepping Thread_Data.var;
 
 fun get_stepping () = the_default (Stepping (false, ~1)) (Thread_Data.get stepping_var);
 fun put_stepping stepping = Thread_Data.put stepping_var (SOME (Stepping stepping));
 
 fun is_stepping () =
   let
     val stack = PolyML.DebuggerInterface.debugState (Thread.self ());
     val Stepping (stepping, depth) = get_stepping ();
   in stepping andalso (depth < 0 orelse length stack <= depth) end;
 
 fun continue () = put_stepping (false, ~1);
 fun step () = put_stepping (true, ~1);
 fun step_over () = put_stepping (true, length (get_debugging ()));
 fun step_out () = put_stepping (true, length (get_debugging ()) - 1);
 
 
 
 (** eval ML **)
 
 local
 
 val context_attempts =
   map ML_Lex.read
    ["Context.put_generic_context (SOME (Context.Theory ML_context))",
     "Context.put_generic_context (SOME (Context.Proof ML_context))",
     "Context.put_generic_context (SOME ML_context)"];
 
 fun environment SML = if SML then ML_Env.SML else ML_Env.Isabelle;
 fun operations SML = if SML then ML_Env.SML_operations else ML_Env.Isabelle_operations;
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
     {environment = environment SML, redirect = false, verbose = verbose,
       debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;
 
 fun eval_setup thread_name index SML context =
   context
   |> Context_Position.set_visible_generic false
   |> ML_Env.add_name_space (environment SML)
       (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
 
 fun eval_context thread_name index SML toks =
   let
     val context = Context.the_generic_context ();
     val context1 =
       if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
       then context
       else
         let
           val context' = context
             |> eval_setup thread_name index SML
             |> ML_Context.exec (fn () =>
                 evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks));
           fun try_exec toks =
             try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
         in
           (case get_first try_exec context_attempts of
             SOME context2 => context2
           | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
         end;
   in context1 |> eval_setup thread_name index SML end;
 
 in
 
 fun eval thread_name index SML txt1 txt2 =
   let
     val (toks1, toks2) = apply2 (#read_source (operations SML) o Input.string) (txt1, txt2);
     val context = eval_context thread_name index SML toks1;
   in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
 
 fun print_vals thread_name index SML txt =
   let
     val toks = #read_source (operations SML) (Input.string txt)
     val context = eval_context thread_name index SML toks;
     val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);
 
     fun print x =
       Pretty.from_polyml
         (PolyML.NameSpace.Values.printWithType
           (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space));
     fun print_all () =
       #allVal (PolyML.DebuggerInterface.debugLocalNameSpace (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)
       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   in Context.setmp_generic_context (SOME context) print_all () end;
 
 end;
 
 
 
 (** debugger loop **)
 
 local
 
 fun debugger_state thread_name =
   Output.protocol_message (Markup.debugger_state thread_name)
-   (get_debugging ()
+   [get_debugging ()
     |> map (fn st =>
       (Position.properties_of
         (Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)),
        PolyML.DebuggerInterface.debugFunction st))
-    |> let open XML.Encode in list (pair properties string) end);
+    |> let open XML.Encode in list (pair properties string) end];
 
 fun debugger_command thread_name =
   (case get_input thread_name of
     [] => (continue (); false)
   | ["continue"] => (continue (); false)
   | ["step"] => (step (); false)
   | ["step_over"] => (step_over (); false)
   | ["step_out"] => (step_out (); false)
   | ["eval", index, SML, txt1, txt2] =>
      (error_wrapper (fn () =>
         eval thread_name (Value.parse_int index) (Value.parse_bool SML) txt1 txt2); true)
   | ["print_vals", index, SML, txt] =>
      (error_wrapper (fn () =>
         print_vals thread_name (Value.parse_int index) (Value.parse_bool SML) txt); true)
   | bad =>
      (Output.system_message
         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
 
 in
 
 fun debugger_loop thread_name =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       fun loop () =
         (debugger_state thread_name; if debugger_command thread_name then loop () else ());
       val result = Exn.capture (restore_attributes with_debugging) loop;
       val _ = debugger_state thread_name;
     in Exn.release result end) ();
 
 end;
 
 
 
 (** protocol commands **)
 
 val _ =
   Protocol_Command.define "Debugger.init"
     (fn [] =>
      (init_input ();
       PolyML.DebuggerInterface.setOnBreakPoint
         (SOME (fn (_, break) =>
           if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
           then
             (case try Isabelle_Thread.get_name () of
               SOME thread_name => debugger_loop thread_name
             | NONE => ())
           else ()))));
 
 val _ =
   Protocol_Command.define "Debugger.exit"
     (fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ()));
 
 val _ =
   Protocol_Command.define "Debugger.break"
     (fn [b] => set_break (Value.parse_bool b));
 
 val _ =
   Protocol_Command.define "Debugger.breakpoint"
     (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
       let
         val id = Value.parse_int id0;
         val breakpoint = Value.parse_int breakpoint0;
         val breakpoint_state = Value.parse_bool breakpoint_state0;
 
         fun err () = error ("Bad exec for command " ^ Value.print_int id);
       in
         (case Document.command_exec (Document.state ()) node_name id of
           SOME (eval, _) =>
             if Command.eval_finished eval then
               let
                 val st = Command.eval_result_state eval;
                 val ctxt = Toplevel.presentation_context st;
               in
                 (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
                   SOME (b, _) => b := breakpoint_state
                 | NONE => err ())
               end
             else err ()
         | NONE => err ())
       end);
 
 val _ =
   Protocol_Command.define "Debugger.input"
     (fn thread_name :: msg => input thread_name msg);
 
 end;
diff --git a/src/Pure/Tools/debugger.scala b/src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala
+++ b/src/Pure/Tools/debugger.scala
@@ -1,296 +1,296 @@
 /*  Title:      Pure/Tools/debugger.scala
     Author:     Makarius
 
 Interactive debugger for Isabelle/ML.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedMap
 
 
 object Debugger
 {
   /* thread context */
 
   case object Update
 
   sealed case class Debug_State(pos: Position.T, function: String)
   type Threads = SortedMap[String, List[Debug_State]]
 
   sealed case class Context(thread_name: String, debug_states: List[Debug_State], index: Int = 0)
   {
     def size: Int = debug_states.length + 1
     def reset: Context = copy(index = 0)
     def select(i: Int): Context = copy(index = i + 1)
 
     def thread_state: Option[Debug_State] = debug_states.headOption
 
     def stack_state: Option[Debug_State] =
       if (1 <= index && index <= debug_states.length)
         Some(debug_states(index - 1))
       else None
 
     def debug_index: Option[Int] =
       if (stack_state.isDefined) Some(index - 1)
       else if (debug_states.nonEmpty) Some(0)
       else None
 
     def debug_state: Option[Debug_State] = stack_state orElse thread_state
     def debug_position: Option[Position.T] = debug_state.map(_.pos)
 
     override def toString: String =
       stack_state match {
         case None => thread_name
         case Some(d) => d.function
       }
   }
 
 
   /* debugger state */
 
   sealed case class State(
     active: Int = 0,  // active views
     break: Boolean = false,  // break at next possible breakpoint
     active_breakpoints: Set[Long] = Set.empty,  // explicit breakpoint state
     threads: Threads = SortedMap.empty,  // thread name ~> stack of debug states
     focus: Map[String, Context] = Map.empty,  // thread name ~> focus
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
   {
     def set_break(b: Boolean): State = copy(break = b)
 
     def is_active: Boolean = active > 0
     def inc_active: State = copy(active = active + 1)
     def dec_active: State = copy(active = active - 1)
 
     def toggle_breakpoint(breakpoint: Long): (Boolean, State) =
     {
       val active_breakpoints1 =
         if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint
       else active_breakpoints + breakpoint
       (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
     }
 
     def get_thread(thread_name: String): List[Debug_State] =
       threads.getOrElse(thread_name, Nil)
 
     def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
     {
       val threads1 =
         if (debug_states.nonEmpty) threads + (thread_name -> debug_states)
         else threads - thread_name
       val focus1 =
         focus.get(thread_name) match {
           case Some(c) if debug_states.nonEmpty =>
             focus + (thread_name -> Context(thread_name, debug_states))
           case _ => focus - thread_name
         }
       copy(threads = threads1, focus = focus1)
     }
 
     def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c))
 
     def get_output(thread_name: String): Command.Results =
       output.getOrElse(thread_name, Command.Results.empty)
 
     def add_output(thread_name: String, entry: Command.Results.Entry): State =
       copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
 
     def clear_output(thread_name: String): State =
       copy(output = output - thread_name)
   }
 
 
   /* protocol handler */
 
   class Handler(session: Session) extends Session.Protocol_Handler
   {
     val debugger: Debugger = new Debugger(session)
 
     private def debugger_state(msg: Prover.Protocol_Output): Boolean =
     {
       msg.properties match {
         case Markup.Debugger_State(thread_name) =>
-          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
+          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.chunk))
           val debug_states =
           {
             import XML.Decode._
             list(pair(properties, string))(msg_body).map({
               case (pos, function) => Debug_State(pos, function)
             })
           }
           debugger.update_thread(thread_name, debug_states)
           true
         case _ => false
       }
     }
 
     private def debugger_output(msg: Prover.Protocol_Output): Boolean =
     {
       msg.properties match {
         case Markup.Debugger_Output(thread_name) =>
-          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
+          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.chunk)) match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
               val message = XML.Elem(Markup(Markup.message(name), props), body)
               debugger.add_output(thread_name, i -> session.cache.elem(message))
               true
             case _ => false
           }
         case _ => false
       }
     }
 
     override val functions =
       List(
         Markup.DEBUGGER_STATE -> debugger_state,
         Markup.DEBUGGER_OUTPUT -> debugger_output)
   }
 }
 
 class Debugger private(session: Session)
 {
   /* debugger state */
 
   private val state = Synchronized(Debugger.State())
 
   private val delay_update =
     Delay.first(session.output_delay) {
       session.debugger_updates.post(Debugger.Update)
     }
 
 
   /* protocol commands */
 
   def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State]): Unit =
   {
     state.change(_.update_thread(thread_name, debug_states))
     delay_update.invoke()
   }
 
   def add_output(thread_name: String, entry: Command.Results.Entry): Unit =
   {
     state.change(_.add_output(thread_name, entry))
     delay_update.invoke()
   }
 
   def is_active(): Boolean = session.is_ready && state.value.is_active
 
   def ready(): Unit =
   {
     if (is_active())
       session.protocol_command("Debugger.init")
   }
 
   def init(): Unit =
     state.change(st =>
     {
       val st1 = st.inc_active
       if (session.is_ready && !st.is_active && st1.is_active)
         session.protocol_command("Debugger.init")
       st1
     })
 
   def exit(): Unit =
     state.change(st =>
     {
       val st1 = st.dec_active
       if (session.is_ready && st.is_active && !st1.is_active)
         session.protocol_command("Debugger.exit")
       st1
     })
 
   def is_break(): Boolean = state.value.break
   def set_break(b: Boolean): Unit =
   {
     state.change(st => {
       val st1 = st.set_break(b)
       session.protocol_command("Debugger.break", b.toString)
       st1
     })
     delay_update.invoke()
   }
 
   def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
   {
     val st = state.value
     if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None
   }
 
   def breakpoint_state(breakpoint: Long): Boolean =
     state.value.active_breakpoints(breakpoint)
 
   def toggle_breakpoint(command: Command, breakpoint: Long): Unit =
   {
     state.change(st =>
       {
         val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint)
         session.protocol_command(
           "Debugger.breakpoint",
           Symbol.encode(command.node_name.node),
           Document_ID(command.id),
           Value.Long(breakpoint),
           Value.Boolean(breakpoint_state))
         st1
       })
   }
 
   def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) =
   {
     val st = state.value
     val output =
       focus match {
         case None => Nil
         case Some(c) =>
           (for {
             (thread_name, results) <- st.output
             if thread_name == c.thread_name
             (_, tree) <- results.iterator
           } yield tree).toList
       }
     (st.threads, output)
   }
 
   def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2)
   def set_focus(c: Debugger.Context): Unit =
   {
     state.change(_.set_focus(c))
     delay_update.invoke()
   }
 
   def input(thread_name: String, msg: String*): Unit =
     session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
 
   def continue(thread_name: String): Unit = input(thread_name, "continue")
   def step(thread_name: String): Unit = input(thread_name, "step")
   def step_over(thread_name: String): Unit = input(thread_name, "step_over")
   def step_out(thread_name: String): Unit = input(thread_name, "step_out")
 
   def clear_output(thread_name: String): Unit =
   {
     state.change(_.clear_output(thread_name))
     delay_update.invoke()
   }
 
   def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String): Unit =
   {
     state.change(st => {
       input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString,
         SML.toString, Symbol.encode(context), Symbol.encode(expression))
       st.clear_output(c.thread_name)
     })
     delay_update.invoke()
   }
 
   def print_vals(c: Debugger.Context, SML: Boolean, context: String): Unit =
   {
     require(c.debug_index.isDefined)
 
     state.change(st => {
       input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString,
         SML.toString, Symbol.encode(context))
       st.clear_output(c.thread_name)
     })
     delay_update.invoke()
   }
 }
diff --git a/src/Pure/Tools/print_operation.ML b/src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML
+++ b/src/Pure/Tools/print_operation.ML
@@ -1,73 +1,73 @@
 (*  Title:      Pure/Tools/print_operation.ML
     Author:     Makarius
 
 Print operations as asynchronous query.
 *)
 
 
 signature PRINT_OPERATION =
 sig
   val register: string -> string -> (Toplevel.state -> Pretty.T list) -> unit
 end;
 
 structure Print_Operation: PRINT_OPERATION =
 struct
 
 (* maintain print operations *)
 
 local
 
 val print_operations =
   Synchronized.var "print_operations"
     ([]: (string * (string * (Toplevel.state -> Pretty.T list))) list);
 
 fun report () =
   Output.try_protocol_message Markup.print_operations
-    (Synchronized.value print_operations
+    [Synchronized.value print_operations
       |> map (fn (x, (y, _)) => (x, y)) |> rev
-      |> let open XML.Encode in list (pair string string) end);
+      |> let open XML.Encode in list (pair string string) end];
 
 val _ = Protocol_Command.define "print_operations" (fn [] => report ());
 
 in
 
 fun register name description pr =
  (Synchronized.change print_operations (fn tab =>
    (if not (AList.defined (op =) tab name) then ()
     else warning ("Redefining print operation: " ^ quote name);
     AList.update (op =) (name, (description, pr)) tab));
   report ());
 
 val _ =
   Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
     (fn {state, args, writeln_result, ...} =>
       let
         val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
         fun err s = Pretty.mark_str (Markup.bad (), s);
         fun print name =
           (case AList.lookup (op =) (Synchronized.value print_operations) name of
             SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
           | NONE => [err ("Unknown print operation: " ^ quote name)]);
       in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
 
 end;
 
 
 (* common print operations *)
 
 val _ =
   register "context" "context of local theory target" Toplevel.pretty_context;
 
 val _ =
   register "cases" "cases of proof context"
     (Proof_Context.pretty_cases o Toplevel.context_of);
 
 val _ =
   register "terms" "term bindings of proof context"
     (Proof_Context.pretty_term_bindings o Toplevel.context_of);
 
 val _ =
   register "theorems" "theorems of local theory or proof context"
     (Isar_Cmd.pretty_theorems false);
 
 end;