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  

     2.1 --- a/src/Pure/General/output.ML	Mon Oct 25 16:52:20 2010 +0200
     2.2 +++ b/src/Pure/General/output.ML	Mon Oct 25 20:24:13 2010 +0200
     2.3 @@ -6,7 +6,6 @@
     2.4  
     2.5  signature BASIC_OUTPUT =
     2.6  sig
     2.7 -  type output = string
     2.8    val writeln: string -> unit
     2.9    val priority: string -> unit
    2.10    val tracing: string -> unit
    2.11 @@ -22,6 +21,7 @@
    2.12  signature OUTPUT =
    2.13  sig
    2.14    include BASIC_OUTPUT
    2.15 +  type output = string
    2.16    val default_output: string -> output * int
    2.17    val default_escape: output -> string
    2.18    val add_mode: string -> (string -> output * int) -> (output -> string) -> unit

     3.1 --- a/src/Pure/General/pretty.ML	Mon Oct 25 16:52:20 2010 +0200
     3.2 +++ b/src/Pure/General/pretty.ML	Mon Oct 25 20:24:13 2010 +0200
     3.3 @@ -21,8 +21,8 @@
     3.4  
     3.5  signature PRETTY =
     3.6  sig
     3.7 -  val default_indent: string -> int -> output
     3.8 -  val add_mode: string -> (string -> int -> output) -> unit
     3.9 +  val default_indent: string -> int -> Output.output
    3.10 +  val add_mode: string -> (string -> int -> Output.output) -> unit
    3.11    type T
    3.12    val str: string -> T
    3.13    val brk: int -> T
    3.14 @@ -55,7 +55,7 @@
    3.15    val margin_default: int Unsynchronized.ref
    3.16    val symbolicN: string
    3.17    val output_buffer: int option -> T -> Buffer.T
    3.18 -  val output: int option -> T -> output
    3.19 +  val output: int option -> T -> Output.output
    3.20    val string_of_margin: int -> T -> string
    3.21    val string_of: T -> string
    3.22    val str_of: T -> string
    3.23 @@ -103,9 +103,10 @@
    3.24  (** printing items: compound phrases, strings, and breaks **)
    3.25  
    3.26  abstype T =
    3.27 -  Block of (output * output) * T list * int * int |  (*markup output, body, indentation, length*)
    3.28 -  String of output * int |                           (*text, length*)
    3.29 -  Break of bool * int                                (*mandatory flag, width if not taken*)
    3.30 +    Block of (Output.output * Output.output) * T list * int * int
    3.31 +      (*markup output, body, indentation, length*)
    3.32 +  | String of Output.output * int  (*text, length*)
    3.33 +  | Break of bool * int  (*mandatory flag, width if not taken*)
    3.34  with
    3.35  
    3.36  fun length (Block (_, _, _, len)) = len

     4.1 --- a/src/Pure/General/symbol.ML	Mon Oct 25 16:52:20 2010 +0200
     4.2 +++ b/src/Pure/General/symbol.ML	Mon Oct 25 20:24:13 2010 +0200
     4.3 @@ -66,7 +66,7 @@
     4.4    val bump_string: string -> string
     4.5    val length: symbol list -> int
     4.6    val xsymbolsN: string
     4.7 -  val output: string -> output * int
     4.8 +  val output: string -> Output.output * int
     4.9  end;
    4.10  
    4.11  structure Symbol: SYMBOL =

     5.1 --- a/src/Pure/General/xml.ML	Mon Oct 25 16:52:20 2010 +0200
     5.2 +++ b/src/Pure/General/xml.ML	Mon Oct 25 20:24:13 2010 +0200
     5.3 @@ -16,7 +16,7 @@
     5.4    val header: string
     5.5    val text: string -> string
     5.6    val element: string -> attributes -> string list -> string
     5.7 -  val output_markup: Markup.T -> output * output
     5.8 +  val output_markup: Markup.T -> Output.output * Output.output
     5.9    val string_of: tree -> string
    5.10    val output: tree -> TextIO.outstream -> unit
    5.11    val parse_comments: string list -> unit * string list

     6.1 --- a/src/Pure/Thy/thy_syntax.ML	Mon Oct 25 16:52:20 2010 +0200
     6.2 +++ b/src/Pure/Thy/thy_syntax.ML	Mon Oct 25 20:24:13 2010 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4      (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
     6.5        Source.source) Source.source) Source.source) Source.source
     6.6    val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
     6.7 -  val present_token: Token.T -> output
     6.8 +  val present_token: Token.T -> Output.output
     6.9    val report_token: Token.T -> unit
    6.10    datatype span_kind = Command of string | Ignored | Malformed
    6.11    type span
    6.12 @@ -19,7 +19,7 @@
    6.13    val span_range: span -> Position.range
    6.14    val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
    6.15    val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
    6.16 -  val present_span: span -> output
    6.17 +  val present_span: span -> Output.output
    6.18    val report_span: span -> unit
    6.19    val atom_source: (span, 'a) Source.source ->
    6.20      (span * span list * bool, (span, 'a) Source.source) Source.source