--- 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;
--- 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
--- 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
--- 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 =
--- 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
--- 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