type output = string indicates raw system output;

--- a/src/Pure/General/output.ML	Sun Jul 08 19:52:10 2007 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 09 11:44:20 2007 +0200
@@ -7,6 +7,7 @@
 
 signature BASIC_OUTPUT =
 sig
+  type output = string
   val writeln: string -> unit
   val priority: string -> unit
   val tracing: string -> unit
@@ -24,22 +25,22 @@
 signature OUTPUT =
 sig
   include BASIC_OUTPUT
-  val default_output: string -> string * int
-  val default_escape: string -> string
-  val add_mode: string -> (string -> string * int) -> (string -> string) -> unit
-  val output_width: string -> string * int
-  val output: string -> string
-  val escape: string -> string
-  val std_output: string -> unit
-  val std_error: string -> unit
+  val default_output: string -> output * int
+  val default_escape: output -> string
+  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
+  val output_width: string -> output * int
+  val output: string -> output
+  val escape: output -> string
+  val std_output: output -> unit
+  val std_error: output -> unit
   val immediate_output: string -> unit
-  val writeln_default: string -> unit
-  val writeln_fn: (string -> unit) ref
-  val priority_fn: (string -> unit) ref
-  val tracing_fn: (string -> unit) ref
-  val warning_fn: (string -> unit) ref
-  val error_fn: (string -> unit) ref
-  val debug_fn: (string -> unit) ref
+  val writeln_default: output -> unit
+  val writeln_fn: (output -> unit) ref
+  val priority_fn: (output -> unit) ref
+  val tracing_fn: (output -> unit) ref
+  val warning_fn: (output -> unit) ref
+  val error_fn: (output -> unit) ref
+  val debug_fn: (output -> unit) ref
   val debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   exception TOPLEVEL_ERROR
@@ -57,8 +58,10 @@
 
 (** print modes **)
 
+type output = string;  (*raw system output*)
+
 fun default_output s = (s, size s);
-fun default_escape (s: string) = s;
+fun default_escape (s: output) = s;
 
 local
   val default = {output = default_output, escape = default_escape};

--- a/src/Pure/General/pretty.ML	Sun Jul 08 19:52:10 2007 +0200
+++ b/src/Pure/General/pretty.ML	Mon Jul 09 11:44:20 2007 +0200
@@ -20,17 +20,17 @@
 a unit for breaking).
 *)
 
-type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
+type pprint_args = (output -> unit) * (int -> unit) * (int -> unit) *
   (unit -> unit) * (unit -> unit);
 
 signature PRETTY =
 sig
-  val default_indent: string -> int -> string
-  val default_markup: Markup.T -> string * string
-  val mode_markup: Markup.T -> string * string
-  val add_mode: string -> (string -> int -> string) -> (Markup.T -> string * string) -> unit
+  val default_indent: string -> int -> output
+  val default_markup: Markup.T -> output * output
+  val mode_markup: Markup.T -> output * output
+  val add_mode: string -> (string -> int -> output) -> (Markup.T -> output * output) -> unit
   type T
-  val raw_str: string * int -> T
+  val raw_str: output * int -> T
   val str: string -> T
   val brk: int -> T
   val fbrk: T
@@ -63,7 +63,7 @@
   val pprint: T -> pprint_args -> unit
   val symbolicN: string
   val output_buffer: T -> Buffer.T
-  val output: T -> string
+  val output: T -> output
   val string_of: T -> string
   val str_of: T -> string
   val writeln: T -> unit
@@ -118,7 +118,7 @@
 
 datatype T =
   Block of Markup.T * T list * int * int |  (*markup, body, indentation, length*)
-  String of string * int |                  (*text, length*)
+  String of output * int |                  (*text, length*)
   Break of bool * int;                      (*mandatory flag, width if not taken*)
 
 fun length (Block (_, _, _, len)) = len

--- a/src/Pure/Isar/isar_cmd.ML	Sun Jul 08 19:52:10 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Jul 09 11:44:20 2007 +0200
@@ -184,7 +184,7 @@
   |> Context.theory_map;
 
 val token_translation =
-  ML_Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
+  ML_Context.use_let "val token_translation: (string * string * (string -> output * int)) list"
     "Context.map_theory (Sign.add_tokentrfuns token_translation)"
   #> Context.theory_map;
 

--- a/src/Pure/Syntax/printer.ML	Sun Jul 08 19:52:10 2007 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Jul 09 11:44:20 2007 +0200
@@ -31,10 +31,10 @@
   val merge_prtabs: prtabs -> prtabs -> prtabs
   val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
     -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
-    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T list
+    -> (string -> (string -> output * int) option) -> Ast.ast -> Pretty.T list
   val pretty_typ_ast: Proof.context -> bool -> prtabs
     -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
-    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T list
+    -> (string -> (string -> output * int) option) -> Ast.ast -> Pretty.T list
 end;
 
 structure Printer: PRINTER =

--- a/src/Pure/Syntax/syn_ext.ML	Sun Jul 08 19:52:10 2007 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Mon Jul 09 11:44:20 2007 +0200
@@ -14,8 +14,8 @@
   val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
   val mk_trfun: string * 'a -> string * ('a * stamp)
   val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
-  val tokentrans_mode: string -> (string * (string -> string * int)) list ->
-    (string * string * (string -> string * int)) list
+  val tokentrans_mode: string -> (string * (string -> output * int)) list ->
+    (string * string * (string -> output * int)) list
   val standard_token_classes: string list
 end;
 
@@ -49,7 +49,7 @@
         (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
       print_rules: (Ast.ast * Ast.ast) list,
       print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
-      token_translation: (string * string * (string -> string * int)) list}
+      token_translation: (string * string * (string -> output * int)) list}
   val mfix_delims: string -> string list
   val mfix_args: string -> int
   val escape_mfix: string -> string
@@ -59,14 +59,14 @@
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
-    -> (string * string * (string -> string * int)) list
+    -> (string * string * (string -> output * int)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext: mfix list -> string list ->
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
-    -> (string * string * (string -> string * int)) list
+    -> (string * string * (string -> output * int)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_const_names: string list -> syn_ext
   val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
@@ -80,7 +80,7 @@
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
-  val syn_ext_tokentrfuns: (string * string * (string -> string * int)) list -> syn_ext
+  val syn_ext_tokentrfuns: (string * string * (string -> output * int)) list -> syn_ext
   val standard_token_markers: string list
   val pure_ext: syn_ext
 end;
@@ -343,7 +343,7 @@
       (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
     print_rules: (Ast.ast * Ast.ast) list,
     print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
-    token_translation: (string * string * (string -> string * int)) list};
+    token_translation: (string * string * (string -> output * int)) list};
 
 
 (* syn_ext *)

--- a/src/Pure/Syntax/syntax.ML	Sun Jul 08 19:52:10 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Jul 09 11:44:20 2007 +0200
@@ -55,7 +55,7 @@
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
-  val extend_tokentrfuns: (string * string * (string -> string * int)) list -> syntax -> syntax
+  val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax
   val remove_const_gram: (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val extend_trrules: Proof.context -> (string -> bool) -> syntax ->
@@ -183,7 +183,7 @@
     print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
     print_ruletab: ruletab,
     print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
-    tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
+    tokentrtab: (string * (string * ((string -> output * int) * stamp)) list) list,
     prtabs: Printer.prtabs} * stamp;
 
 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;

--- a/src/Pure/sign.ML	Sun Jul 08 19:52:10 2007 +0200
+++ b/src/Pure/sign.ML	Mon Jul 09 11:44:20 2007 +0200
@@ -38,8 +38,8 @@
   val add_advanced_trfunsT:
     (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
   val add_tokentrfuns:
-    (string * string * (string -> string * int)) list -> theory -> theory
-  val add_mode_tokentrfuns: string -> (string * (string -> string * int)) list
+    (string * string * (string -> output * int)) list -> theory -> theory
+  val add_mode_tokentrfuns: string -> (string * (string -> output * int)) list
     -> theory -> theory
   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
   val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory