# HG changeset patch
# User paulson
# Date 1572705108 0
# Node ID 98308c6582edb651bb2c704c2ad3afc9552dcd80
# Parent  7926d2fc3c4c7fca137578b4750ca117e690e703# Parent  5b753486c075578c90c78c79639f6854c1bf34e8
merged

diff -r 5b753486c075 -r 98308c6582ed src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -973,8 +973,8 @@
           val prv_path = Path.ext "prv" path;
           val _ =
             Export.export thy (Path.binding (prv_path, Position.none))
-              [implode (map (fn (s, _) => snd (strip_number s) ^
-                " -- proved by " ^ Distribution.version ^ "\n") proved'')];
+              (proved'' |> map (fn (s, _) =>
+                XML.Text (snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n")));
         in {pfuns = pfuns, type_map = type_map, env = NONE} end))
   |> Sign.parent_path;
 
diff -r 5b753486c075 -r 98308c6582ed src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/General/buffer.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -9,48 +9,28 @@
   type T
   val empty: T
   val is_empty: T -> bool
-  val chunks: T -> string list
   val content: T -> string
   val add: string -> T -> T
+  val output: T -> (string -> unit) -> unit
   val markup: Markup.T -> (T -> T) -> T -> T
-  val output: T -> BinIO.outstream -> unit
 end;
 
 structure Buffer: BUFFER =
 struct
 
-abstype T = Buffer of {chunk_size: int, chunk: string list, buffer: string list}
+abstype T = Buffer of string list
 with
 
-val empty = Buffer {chunk_size = 0, chunk = [], buffer = []};
-
-fun is_empty (Buffer {chunk, buffer, ...}) = null chunk andalso null buffer;
-
-local
-  val chunk_limit = 4096;
+val empty = Buffer [];
 
-  fun add_chunk [] buffer = buffer
-    | add_chunk chunk buffer = implode (rev chunk) :: buffer;
-in
-
-fun chunks (Buffer {chunk, buffer, ...}) = rev (add_chunk chunk buffer);
-
-val content = implode o chunks;
+fun is_empty (Buffer xs) = null xs;
 
-fun add x (buf as Buffer {chunk_size, chunk, buffer}) =
-  let val n = size x in
-    if n = 0 then buf
-    else if n + chunk_size < chunk_limit then
-      Buffer {chunk_size = n + chunk_size, chunk = x :: chunk, buffer = buffer}
-    else
-      Buffer {chunk_size = 0, chunk = [],
-        buffer =
-          if n < chunk_limit
-          then add_chunk (x :: chunk) buffer
-          else x :: add_chunk chunk buffer}
-  end;
+fun add "" buf = buf
+  | add x (Buffer xs) = Buffer (x :: xs);
 
-end;
+fun content (Buffer xs) = implode (rev xs);
+
+fun output (Buffer xs) out = List.app out (rev xs);
 
 end;
 
@@ -58,7 +38,4 @@
   let val (bg, en) = Markup.output m
   in add bg #> body #> add en end;
 
-fun output buf stream =
-  List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (chunks buf);
-
 end;
diff -r 5b753486c075 -r 98308c6582ed src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/General/file.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -165,7 +165,7 @@
 fun append path txt = append_list path [txt];
 fun generate path txt = if try read path = SOME txt then () else write path txt;
 
-fun write_buffer path buf = open_output (Buffer.output buf) path;
+fun write_buffer path buf = open_output (Buffer.output buf o output) path;
 
 
 (* eq *)
diff -r 5b753486c075 -r 98308c6582ed src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/General/output.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -28,8 +28,9 @@
   val physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
+  type protocol_message_fn = Output_Primitives.protocol_message_fn
   exception Protocol_Message of Properties.T
-  val protocol_message_undefined: Properties.T -> string list -> unit
+  val protocol_message_undefined: protocol_message_fn
   val writelns: string list -> unit
   val state: string -> unit
   val information: string -> unit
@@ -39,8 +40,8 @@
   val status: string list -> unit
   val report: string list -> unit
   val result: Properties.T -> string list -> unit
-  val protocol_message: Properties.T -> string list -> unit
-  val try_protocol_message: Properties.T -> string list -> unit
+  val protocol_message: protocol_message_fn
+  val try_protocol_message: protocol_message_fn
 end;
 
 signature PRIVATE_OUTPUT =
@@ -57,7 +58,7 @@
   val status_fn: (output list -> unit) Unsynchronized.ref
   val report_fn: (output list -> unit) Unsynchronized.ref
   val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
-  val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
+  val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref
   val init_channels: unit -> unit
 end;
 
@@ -105,6 +106,8 @@
 val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
 val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
 val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
+
+type protocol_message_fn = Output_Primitives.protocol_message_fn;
 val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
 
 
@@ -121,8 +124,8 @@
 
 exception Protocol_Message of Properties.T;
 
-fun protocol_message_undefined props (_: string list) =
-  raise Protocol_Message props;
+val protocol_message_undefined: Output_Primitives.protocol_message_fn =
+  fn props => fn _ => raise Protocol_Message props;
 
 fun init_channels () =
  (writeln_fn := (physical_writeln o implode);
@@ -153,8 +156,8 @@
 fun status ss = ! status_fn (map output ss);
 fun report ss = ! report_fn (map output ss);
 fun result props ss = ! result_fn props (map output ss);
-fun protocol_message props ss = ! protocol_message_fn props (map output ss);
-fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
+fun protocol_message props body = ! protocol_message_fn props body;
+fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
 
 
 (* profiling *)
diff -r 5b753486c075 -r 98308c6582ed src/Pure/General/output_primitives.ML
--- a/src/Pure/General/output_primitives.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/General/output_primitives.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -6,6 +6,14 @@
 
 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
@@ -21,13 +29,31 @@
   val status_fn: output list -> unit
   val report_fn: output list -> unit
   val result_fn: properties -> output list -> unit
-  val protocol_message_fn: properties -> output list -> unit
+  type protocol_message_fn = properties -> XML.body -> 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;
@@ -45,7 +71,9 @@
 val status_fn = ignore_outputs;
 val report_fn = ignore_outputs;
 fun result_fn (_: properties) = ignore_outputs;
-fun protocol_message_fn (_: properties) = ignore_outputs;
+
+type protocol_message_fn = properties -> XML.body -> unit;
+val protocol_message_fn: protocol_message_fn = fn _ => fn _ => ();
 
 fun markup_fn (_: string * properties) = ("", "");
 
diff -r 5b753486c075 -r 98308c6582ed src/Pure/PIDE/byte_message.ML
--- a/src/Pure/PIDE/byte_message.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/PIDE/byte_message.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -23,7 +23,7 @@
 
 (* output operations *)
 
-fun write stream = List.app (fn s => BinIO.output (stream, Byte.stringToBytes s));
+fun write stream = List.app (File.output stream);
 
 fun flush stream = ignore (try BinIO.flushOut stream);
 
diff -r 5b753486c075 -r 98308c6582ed src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/PIDE/protocol.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -62,7 +62,7 @@
     tokens = toks ~~ sources}
   end;
 
-fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [commas ids];
+fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [XML.Text (commas ids)];
 
 val _ =
   Isabelle_Process.protocol_command "Document.define_command"
@@ -146,8 +146,7 @@
                     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
-                  |> YXML.chunks_of_body);
+                  in triple int (list string) (list encode_upd) end);
           in Document.start_execution state' end)));
 
 val _ =
@@ -158,7 +157,7 @@
           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 [versions_yxml];
+        val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)];
       in state1 end));
 
 val _ =
diff -r 5b753486c075 -r 98308c6582ed src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/PIDE/xml.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -34,6 +34,9 @@
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
+  val blob: string list -> body
+  val is_empty: tree -> bool
+  val is_empty_body: body -> bool
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
@@ -48,7 +51,6 @@
   val output_markup: Markup.T -> Markup.output
   val string_of: tree -> string
   val pretty: int -> tree -> Pretty.T
-  val output: tree -> BinIO.outstream -> unit
   val parse_comments: string list -> unit * string list
   val parse_string : string -> string option
   val parse_element: string list -> tree * string list
@@ -73,13 +75,14 @@
 
 (** XML trees **)
 
-type attributes = (string * string) list;
+open Output_Primitives.XML;
+
+val blob = map Text;
 
-datatype tree =
-    Elem of (string * attributes) * tree list
-  | Text of string;
+fun is_empty (Text "") = true
+  | is_empty _ = false;
 
-type body = tree list;
+val is_empty_body = forall is_empty;
 
 
 (* wrapped elements *)
@@ -177,7 +180,6 @@
   in Buffer.empty |> traverse depth tree end;
 
 val string_of = Buffer.content o buffer_of ~1;
-val output = Buffer.output o buffer_of ~1;
 
 fun pretty depth tree =
   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
diff -r 5b753486c075 -r 98308c6582ed src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/PIDE/yxml.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -20,12 +20,11 @@
   val Y: Symbol.symbol
   val embed_controls: string -> string
   val detect: string -> bool
-  val output_markup: Markup.T -> string * string
-  val buffer_body: XML.body -> Buffer.T -> Buffer.T
-  val buffer: XML.tree -> Buffer.T -> Buffer.T
-  val chunks_of_body: XML.body -> string list
+  val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
+  val write_body: Path.T -> XML.body -> unit
+  val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
@@ -65,30 +64,33 @@
 
 (* output *)
 
+fun traverse string =
+  let
+    fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
+    fun tree (XML.Elem ((name, atts), ts)) =
+          string XY #> string name #> fold attrib atts #> string X #>
+          fold tree ts #>
+          string XYX
+      | tree (XML.Text s) = string s;
+  in tree end;
+
+fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
+val string_of = string_of_body o single;
+
+fun write_body path body =
+  path |> File.open_output (fn file =>
+    fold (traverse (fn s => fn () => File.output file s)) body ());
+
+
+(* markup elements *)
+
+val Z = chr 0;
+val Z_text = [XML.Text Z];
+
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
-fun buffer_attrib (a, x) =
-  Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
-
-fun buffer_body ts = fold buffer ts
-and buffer (XML.Elem ((name, atts), ts)) =
-      Buffer.add XY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add X #>
-      buffer_body ts #>
-      Buffer.add XYX
-  | buffer (XML.Text s) = Buffer.add s
-
-fun chunks_of_body body = Buffer.empty |> buffer_body body |> Buffer.chunks;
-fun string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content;
-val string_of = string_of_body o single;
-
-
-(* wrapped elements *)
-
-val Z = chr 0;
-val Z_text = [XML.Text Z];
-
 fun output_markup_elem markup =
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
   in ((bg1, bg2), en) end;
diff -r 5b753486c075 -r 98308c6582ed src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/System/invoke_scala.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -33,7 +33,7 @@
     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
     val promise = Future.promise_name "invoke_scala" abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
-    val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
+    val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
   in promise end;
 
 fun method name arg = Future.join (promise_method name arg);
diff -r 5b753486c075 -r 98308c6582ed src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/System/isabelle_process.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -106,15 +106,15 @@
     fun message name props body =
       Message_Channel.send msg_channel (Message_Channel.message name props body);
 
-    fun standard_message props name body =
-      if forall (fn s => s = "") body then ()
+    fun standard_message props name ss =
+      if forall (fn s => s = "") ss then ()
       else
         let
           val props' =
             (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
               (false, SOME id') => props @ [(Markup.idN, id')]
             | _ => props);
-        in message name props' body end;
+        in message name props' (XML.blob ss) end;
   in
     Private_Output.status_fn := standard_message [] Markup.statusN;
     Private_Output.report_fn := standard_message [] Markup.reportN;
@@ -130,11 +130,13 @@
     Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
     Private_Output.error_message_fn :=
       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
-    Private_Output.system_message_fn := message Markup.systemN [];
-    Private_Output.protocol_message_fn := message Markup.protocolN;
+    Private_Output.system_message_fn :=
+      (fn ss => message Markup.systemN [] (XML.blob ss));
+    Private_Output.protocol_message_fn :=
+      (fn props => fn body => message Markup.protocolN props body);
 
     Session.init_protocol_handlers ();
-    message Markup.initN [] [Session.welcome ()];
+    message Markup.initN [] [XML.Text (Session.welcome ())];
     msg_channel
   end;
 
diff -r 5b753486c075 -r 98308c6582ed src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/System/message_channel.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -7,7 +7,7 @@
 signature MESSAGE_CHANNEL =
 sig
   type message
-  val message: string -> Properties.T -> string list -> message
+  val message: string -> Properties.T -> XML.body -> message
   type T
   val send: T -> message -> unit
   val shutdown: T -> unit
@@ -19,19 +19,20 @@
 
 (* message *)
 
-datatype message = Message of string list;
+datatype message = Message of XML.body;
 
-fun chunk ss =
-  string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss;
+fun body_size body = fold (YXML.traverse (Integer.add o size)) body 0;
+
+fun chunk body = XML.Text (string_of_int (body_size body) ^ "\n") :: body;
 
 fun message name raw_props body =
   let
     val robust_props = map (apply2 YXML.embed_controls) raw_props;
-    val header = YXML.string_of (XML.Elem ((name, robust_props), []));
+    val header = XML.Elem ((name, robust_props), []);
   in Message (chunk [header] @ chunk body) end;
 
-fun output_message stream (Message ss) =
-  List.app (File.output stream) ss;
+fun output_message stream (Message body) =
+  fold (YXML.traverse (fn s => fn () => File.output stream s)) body ();
 
 
 (* channel *)
diff -r 5b753486c075 -r 98308c6582ed src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Thy/export.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -9,14 +9,14 @@
   val report_export: theory -> Path.binding -> unit
   type params =
     {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
-  val export_params: params -> string list -> unit
-  val export: theory -> Path.binding -> string list -> unit
-  val export_executable: theory -> Path.binding -> string list -> unit
+  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
-  val protocol_message: Properties.T -> string list -> unit
+  val protocol_message: Output.protocol_message_fn
 end;
 
 structure Export: EXPORT =
@@ -34,7 +34,7 @@
 type params =
   {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
 
-fun export_params ({theory = thy, binding, executable, compress, strict}: params) blob =
+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 ()),
@@ -43,18 +43,21 @@
     name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
     compress = compress,
-    strict = strict} blob);
+    strict = strict} body);
 
-fun export thy binding blob =
+fun export thy binding body =
   export_params
-    {theory = thy, binding = binding, executable = false, compress = true, strict = true} blob;
+    {theory = thy, binding = binding, executable = false, compress = true, strict = true} body;
 
-fun export_executable thy binding blob =
+fun export_executable thy binding body =
   export_params
-    {theory = thy, binding = binding, executable = true, compress = true, strict = true} blob;
+    {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
 
-fun export_file thy binding file = export thy binding [File.read file];
-fun export_executable_file thy binding file = export_executable thy binding [File.read file];
+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 *)
@@ -71,7 +74,7 @@
 
 (* protocol message (bootstrap) *)
 
-fun protocol_message props output =
+fun protocol_message props body =
   (case props of
     function :: args =>
       if function = (Markup.functionN, Markup.exportN) andalso
@@ -79,7 +82,7 @@
       then
         let
           val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
-          val _ = File.write_list path output;
+          val _ = YXML.write_body path body;
         in Protocol_Message.inline (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
       else raise Output.Protocol_Message props
   | [] => raise Output.Protocol_Message props);
diff -r 5b753486c075 -r 98308c6582ed src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Thy/export_theory.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -125,12 +125,9 @@
   Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
     if Options.bool (#options context) "export_theory" then f context thy else ()));
 
-fun export_buffer thy name buffer =
-  if Buffer.is_empty buffer then ()
-  else Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks buffer);
-
-fun export_body thy name elems =
-  export_buffer thy name (YXML.buffer_body elems Buffer.empty);
+fun export_body thy name body =
+  if XML.is_empty_body body then ()
+  else Export.export thy (Path.binding0 (Path.make ["theory", name])) body;
 
 
 (* presentation *)
@@ -301,17 +298,13 @@
           in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end
       end;
 
-    fun buffer_export_thm (thm_id, thm_name) =
+    fun export_thm (thm_id, thm_name) =
       let
         val markup = entity_markup_thm (#serial thm_id, thm_name);
         val thm = Global_Theory.get_thm_name thy (thm_name, Position.none);
-        val body = encode_thm thm_id thm;
-      in YXML.buffer (XML.Elem (markup, body)) end;
+      in XML.Elem (markup, encode_thm thm_id thm) end;
 
-    val _ =
-      Buffer.empty
-      |> fold buffer_export_thm (Global_Theory.dest_thm_names thy)
-      |> export_buffer thy "thms";
+    val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy));
 
 
     (* type classes *)
@@ -420,7 +413,7 @@
 
     val _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
-        [YXML.string_of_body (XML.Encode.string (cat_lines (map Context.theory_long_name parents)))];
+        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
 
   in () end);
 
diff -r 5b753486c075 -r 98308c6582ed src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Thy/thy_info.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -65,8 +65,9 @@
             val latex = Latex.isabelle_body (Context.theory_name thy) body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
             val _ =
-              if Options.bool options "export_document"
-              then Export.export thy (Path.explode_binding0 "document.tex") output else ();
+              if Options.bool options "export_document" then
+                Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output)
+              else ();
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));
diff -r 5b753486c075 -r 98308c6582ed src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Tools/build.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -239,11 +239,12 @@
 val _ =
   Isabelle_Process.protocol_command "build_session"
     (fn [args_yxml] =>
-      let
-        val args = decode_args args_yxml;
-        val result = (build_session args; "") handle exn =>
-          (Runtime.exn_message exn handle _ (*sic!*) =>
-            "Exception raised, but failed to print details!");
-    in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
+        let
+          val args = decode_args args_yxml;
+          val result = (build_session args; "") handle exn =>
+            (Runtime.exn_message exn handle _ (*sic!*) =>
+              "Exception raised, but failed to print details!");
+        in Output.protocol_message Markup.build_session_finished [XML.Text result] end
+      | _ => raise Match);
 
 end;
diff -r 5b753486c075 -r 98308c6582ed src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Tools/debugger.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -23,7 +23,7 @@
   else
     Output.protocol_message
       (Markup.debugger_output (Standard_Thread.the_name ()))
-      [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;
@@ -201,13 +201,12 @@
 
 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
-    |> YXML.string_of_body];
+    |> let open XML.Encode in list (pair properties string) end);
 
 fun debugger_command thread_name =
   (case get_input thread_name of
diff -r 5b753486c075 -r 98308c6582ed src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Tools/generated_files.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -136,7 +136,7 @@
   in () end;
 
 fun export_file thy (file: file) =
-  Export.export thy (file_binding file) [#content file];
+  Export.export thy (file_binding file) [XML.Text (#content file)];
 
 
 (* file types *)
@@ -290,7 +290,7 @@
                 Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
             in
               (if is_some executable then Export.export_executable else Export.export)
-                thy binding' [content]
+                thy binding' [XML.Text content]
             end));
       val _ =
         if null export then ()
diff -r 5b753486c075 -r 98308c6582ed src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Tools/print_operation.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -23,13 +23,9 @@
 
 fun report () =
   Output.try_protocol_message Markup.print_operations
-    let
-      val yxml =
-        Synchronized.value print_operations
-        |> map (fn (x, (y, _)) => (x, y)) |> rev
-        |> let open XML.Encode in list (pair string string) end
-        |> YXML.string_of_body;
-    in [yxml] end;
+    (Synchronized.value print_operations
+      |> map (fn (x, (y, _)) => (x, y)) |> rev
+      |> let open XML.Encode in list (pair string string) end);
 
 val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
 
diff -r 5b753486c075 -r 98308c6582ed src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/proofterm.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -2150,14 +2150,13 @@
         val encode_term = encode_standard_term consts;
         val encode_proof = encode_standard_proof consts;
       in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
-    val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in
-    chunks |> Export.export_params
+    Export.export_params
      {theory = thy,
       binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
       executable = false,
       compress = true,
-      strict = false}
+      strict = false} xml
   end;
 
 fun export thy i prop prf =
diff -r 5b753486c075 -r 98308c6582ed src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Tools/Code/code_target.ML	Sat Nov 02 14:31:48 2019 +0000
@@ -282,7 +282,7 @@
 fun export binding content thy =
   let
     val thy' = thy |> Generated_Files.add_files (binding, content);
-    val _ = Export.export thy' binding [content];
+    val _ = Export.export thy' binding [XML.Text content];
   in thy' end;
 
 local