changeset 40131 | 7cbebd636e79 |
parent 39555 | ccb223a4d49c |
child 40627 | becf5d5187cc |
--- a/src/Pure/General/xml.ML Mon Oct 25 16:52:20 2010 +0200 +++ b/src/Pure/General/xml.ML Mon Oct 25 20:24:13 2010 +0200 @@ -16,7 +16,7 @@ val header: string val text: string -> string val element: string -> attributes -> string list -> string - val output_markup: Markup.T -> output * output + val output_markup: Markup.T -> Output.output * Output.output val string_of: tree -> string val output: tree -> TextIO.outstream -> unit val parse_comments: string list -> unit * string list