1.1 --- a/src/Pure/General/markup.ML Mon Oct 25 16:52:20 2010 +0200
1.2 +++ b/src/Pure/General/markup.ML Mon Oct 25 20:24:13 2010 +0200
1.3 @@ -120,11 +120,11 @@
1.4 val reportN: string val report: T
1.5 val no_reportN: string val no_report: T
1.6 val badN: string val bad: T
1.7 - val no_output: output * output
1.8 - val default_output: T -> output * output
1.9 - val add_mode: string -> (T -> output * output) -> unit
1.10 - val output: T -> output * output
1.11 - val enclose: T -> output -> output
1.12 + val no_output: Output.output * Output.output
1.13 + val default_output: T -> Output.output * Output.output
1.14 + val add_mode: string -> (T -> Output.output * Output.output) -> unit
1.15 + val output: T -> Output.output * Output.output
1.16 + val enclose: T -> Output.output -> Output.output
1.17 val markup: T -> string -> string
1.18 end;
1.19