# HG changeset patch
# User wenzelm
# Date 1288031053 -7200
# Node ID 7cbebd636e79aaee14abec88fb87122d6c0027b6
# Parent  db6e84082695ce6bc9c2e2c9c2808425a110f8b7
explicitly qualify type Output.output, which is a slightly odd internal feature;

diff -r db6e84082695 -r 7cbebd636e79 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Oct 25 16:52:20 2010 +0200
+++ b/src/Pure/General/markup.ML	Mon Oct 25 20:24:13 2010 +0200
@@ -120,11 +120,11 @@
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: T
-  val no_output: output * output
-  val default_output: T -> output * output
-  val add_mode: string -> (T -> output * output) -> unit
-  val output: T -> output * output
-  val enclose: T -> output -> output
+  val no_output: Output.output * Output.output
+  val default_output: T -> Output.output * Output.output
+  val add_mode: string -> (T -> Output.output * Output.output) -> unit
+  val output: T -> Output.output * Output.output
+  val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
 end;
 
diff -r db6e84082695 -r 7cbebd636e79 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Oct 25 16:52:20 2010 +0200
+++ b/src/Pure/General/output.ML	Mon Oct 25 20:24:13 2010 +0200
@@ -6,7 +6,6 @@
 
 signature BASIC_OUTPUT =
 sig
-  type output = string
   val writeln: string -> unit
   val priority: string -> unit
   val tracing: string -> unit
@@ -22,6 +21,7 @@
 signature OUTPUT =
 sig
   include BASIC_OUTPUT
+  type output = string
   val default_output: string -> output * int
   val default_escape: output -> string
   val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
diff -r db6e84082695 -r 7cbebd636e79 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Oct 25 16:52:20 2010 +0200
+++ b/src/Pure/General/pretty.ML	Mon Oct 25 20:24:13 2010 +0200
@@ -21,8 +21,8 @@
 
 signature PRETTY =
 sig
-  val default_indent: string -> int -> output
-  val add_mode: string -> (string -> int -> output) -> unit
+  val default_indent: string -> int -> Output.output
+  val add_mode: string -> (string -> int -> Output.output) -> unit
   type T
   val str: string -> T
   val brk: int -> T
@@ -55,7 +55,7 @@
   val margin_default: int Unsynchronized.ref
   val symbolicN: string
   val output_buffer: int option -> T -> Buffer.T
-  val output: int option -> T -> output
+  val output: int option -> T -> Output.output
   val string_of_margin: int -> T -> string
   val string_of: T -> string
   val str_of: T -> string
@@ -103,9 +103,10 @@
 (** printing items: compound phrases, strings, and breaks **)
 
 abstype T =
-  Block of (output * output) * T list * int * int |  (*markup output, body, indentation, length*)
-  String of output * int |                           (*text, length*)
-  Break of bool * int                                (*mandatory flag, width if not taken*)
+    Block of (Output.output * Output.output) * T list * int * int
+      (*markup output, body, indentation, length*)
+  | String of Output.output * int  (*text, length*)
+  | Break of bool * int  (*mandatory flag, width if not taken*)
 with
 
 fun length (Block (_, _, _, len)) = len
diff -r db6e84082695 -r 7cbebd636e79 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Oct 25 16:52:20 2010 +0200
+++ b/src/Pure/General/symbol.ML	Mon Oct 25 20:24:13 2010 +0200
@@ -66,7 +66,7 @@
   val bump_string: string -> string
   val length: symbol list -> int
   val xsymbolsN: string
-  val output: string -> output * int
+  val output: string -> Output.output * int
 end;
 
 structure Symbol: SYMBOL =
diff -r db6e84082695 -r 7cbebd636e79 src/Pure/General/xml.ML
--- 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
diff -r db6e84082695 -r 7cbebd636e79 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Mon Oct 25 16:52:20 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Mon Oct 25 20:24:13 2010 +0200
@@ -10,7 +10,7 @@
     (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
       Source.source) Source.source) Source.source) Source.source
   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
-  val present_token: Token.T -> output
+  val present_token: Token.T -> Output.output
   val report_token: Token.T -> unit
   datatype span_kind = Command of string | Ignored | Malformed
   type span
@@ -19,7 +19,7 @@
   val span_range: span -> Position.range
   val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
-  val present_span: span -> output
+  val present_span: span -> Output.output
   val report_span: span -> unit
   val atom_source: (span, 'a) Source.source ->
     (span * span list * bool, (span, 'a) Source.source) Source.source