src/Pure/General/markup.ML
changeset 40391 7cbebd636e79
parent 39849 00be8711082f
child 40670 b0dafbfc05b7
     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