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,107 +1,107 @@
 (*  Title:      Pure/General/byte_message.ML
     Author:     Makarius
 
 Byte-oriented messages.
 *)
 
 signature BYTE_MESSAGE =
 sig
   val write: BinIO.outstream -> string list -> 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 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 (fn s => BinIO.output (stream, Byte.stringToBytes s));
+fun write stream = List.app (File.output stream);
 
 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 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/yxml.ML b/src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML
+++ b/src/Pure/PIDE/yxml.ML
@@ -1,167 +1,167 @@
 (*  Title:      Pure/PIDE/yxml.ML
     Author:     Makarius
 
 Efficient text representation of XML trees using extra characters X
 and Y -- no escaping, may nest marked text verbatim.  Suitable for
 direct inlining into plain text.
 
 Markup <elem att="val" ...>...body...</elem> is encoded as:
 
   X Y name Y att=val ... X
   ...
   body
   ...
   X Y X
 *)
 
 signature YXML =
 sig
   val X: Symbol.symbol
   val Y: Symbol.symbol
   val embed_controls: string -> string
   val detect: string -> bool
   val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
   val buffer: XML.tree -> Buffer.T -> Buffer.T
   val chunks_of_body: XML.body -> string list
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val write_body: Path.T -> XML.body -> unit
   val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
   val content_of: string -> string
 end;
 
 structure YXML: YXML =
 struct
 
 (** string representation **)
 
 (* idempotent recoding of certain low ASCII control characters *)
 
 fun pseudo_utf8 c =
   if Symbol.is_ascii_control c
   then chr 192 ^ chr (128 + ord c)
   else c;
 
 fun embed_controls str =
   if exists_string Symbol.is_ascii_control str
   then translate_string pseudo_utf8 str
   else str;
 
 
 (* markers *)
 
 val X_char = Char.chr 5;
 val Y_char = Char.chr 6;
 
 val X = String.str X_char;
 val Y = String.str Y_char;
 val XY = X ^ Y;
 val XYX = XY ^ X;
 
 fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
 
 
 (* output *)
 
 fun traverse string =
   let
     fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
     fun tree (XML.Elem ((name, atts), ts)) =
           string XY #> string name #> fold attrib atts #> string X #>
           fold tree ts #>
           string XYX
       | tree (XML.Text s) = string s;
   in tree end;
 
 val buffer = traverse Buffer.add;
 
 fun chunks_of_body body = Buffer.empty |> fold buffer body |> Buffer.chunks;
 fun string_of_body body = Buffer.empty |> fold buffer 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 () => BinIO.output (file, Byte.stringToBytes s))) body ());
+    fold (traverse (fn s => fn () => File.output file s)) body ());
 
 
 (* markup elements *)
 
 val Z = chr 0;
 val Z_text = [XML.Text Z];
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun output_markup_elem markup =
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
   in ((bg1, bg2), en) end;
 
 
 
 (** efficient YXML parsing **)
 
 local
 
 (* splitting *)
 
 val split_string =
   Substring.full #>
   Substring.tokens (fn c => c = X_char) #>
   map (Substring.fields (fn c => c = Y_char) #> map Substring.string);
 
 
 (* structural errors *)
 
 fun err msg = raise Fail ("Malformed YXML: " ^ msg);
 fun err_attribute () = err "bad attribute";
 fun err_element () = err "bad element";
 fun err_unbalanced "" = err "unbalanced element"
   | err_unbalanced name = err ("unbalanced element " ^ quote name);
 
 
 (* stack operations *)
 
 fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
 
 fun push "" _ _ = err_element ()
   | push name atts pending = ((name, atts), []) :: pending;
 
 fun pop ((("", _), _) :: _) = err_unbalanced ""
   | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
 
 
 (* parsing *)
 
 fun parse_attrib s =
   (case first_field "=" s of
     NONE => err_attribute ()
   | SOME ("", _) => err_attribute ()
   | SOME att => att);
 
 fun parse_chunk ["", ""] = pop
   | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
   | parse_chunk txts = fold (add o XML.Text) txts;
 
 in
 
 fun parse_body source =
   (case fold parse_chunk (split_string source) [(("", []), [])] of
     [(("", _), result)] => rev result
   | ((name, _), _) :: _ => err_unbalanced name);
 
 fun parse source =
   (case parse_body source of
     [result] => result
   | [] => XML.Text ""
   | _ => err "multiple results");
 
 end;
 
 val content_of = parse_body #> XML.content_of;
 
 end;