# HG changeset patch
# User wenzelm
# Date 1572697558 -3600
# Node ID 325247f32da94d5d59ff80cf792fda420726e03d
# Parent  ebdfd6c43e563a541e04595a05501d9deee27ba8
unused;

diff -r ebdfd6c43e56 -r 325247f32da9 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sat Nov 02 13:20:37 2019 +0100
+++ b/src/Pure/PIDE/xml.ML	Sat Nov 02 13:25:58 2019 +0100
@@ -51,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
@@ -181,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));