1.1 --- a/src/Pure/General/output.ML	Sun Jul 08 19:52:10 2007 +0200
     1.2 +++ b/src/Pure/General/output.ML	Mon Jul 09 11:44:20 2007 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature BASIC_OUTPUT =
     1.6  sig
     1.7 +  type output = string
     1.8    val writeln: string -> unit
     1.9    val priority: string -> unit
    1.10    val tracing: string -> unit
    1.11 @@ -24,22 +25,22 @@
    1.12  signature OUTPUT =
    1.13  sig
    1.14    include BASIC_OUTPUT
    1.15 -  val default_output: string -> string * int
    1.16 -  val default_escape: string -> string
    1.17 -  val add_mode: string -> (string -> string * int) -> (string -> string) -> unit
    1.18 -  val output_width: string -> string * int
    1.19 -  val output: string -> string
    1.20 -  val escape: string -> string
    1.21 -  val std_output: string -> unit
    1.22 -  val std_error: string -> unit
    1.23 +  val default_output: string -> output * int
    1.24 +  val default_escape: output -> string
    1.25 +  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
    1.26 +  val output_width: string -> output * int
    1.27 +  val output: string -> output
    1.28 +  val escape: output -> string
    1.29 +  val std_output: output -> unit
    1.30 +  val std_error: output -> unit
    1.31    val immediate_output: string -> unit
    1.32 -  val writeln_default: string -> unit
    1.33 -  val writeln_fn: (string -> unit) ref
    1.34 -  val priority_fn: (string -> unit) ref
    1.35 -  val tracing_fn: (string -> unit) ref
    1.36 -  val warning_fn: (string -> unit) ref
    1.37 -  val error_fn: (string -> unit) ref
    1.38 -  val debug_fn: (string -> unit) ref
    1.39 +  val writeln_default: output -> unit
    1.40 +  val writeln_fn: (output -> unit) ref
    1.41 +  val priority_fn: (output -> unit) ref
    1.42 +  val tracing_fn: (output -> unit) ref
    1.43 +  val warning_fn: (output -> unit) ref
    1.44 +  val error_fn: (output -> unit) ref
    1.45 +  val debug_fn: (output -> unit) ref
    1.46    val debugging: bool ref
    1.47    val no_warnings: ('a -> 'b) -> 'a -> 'b
    1.48    exception TOPLEVEL_ERROR
    1.49 @@ -57,8 +58,10 @@
    1.50  
    1.51  (** print modes **)
    1.52  
    1.53 +type output = string;  (*raw system output*)
    1.54 +
    1.55  fun default_output s = (s, size s);
    1.56 -fun default_escape (s: string) = s;
    1.57 +fun default_escape (s: output) = s;
    1.58  
    1.59  local
    1.60    val default = {output = default_output, escape = default_escape};

     2.1 --- a/src/Pure/General/pretty.ML	Sun Jul 08 19:52:10 2007 +0200
     2.2 +++ b/src/Pure/General/pretty.ML	Mon Jul 09 11:44:20 2007 +0200
     2.3 @@ -20,17 +20,17 @@
     2.4  a unit for breaking).
     2.5  *)
     2.6  
     2.7 -type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
     2.8 +type pprint_args = (output -> unit) * (int -> unit) * (int -> unit) *
     2.9    (unit -> unit) * (unit -> unit);
    2.10  
    2.11  signature PRETTY =
    2.12  sig
    2.13 -  val default_indent: string -> int -> string
    2.14 -  val default_markup: Markup.T -> string * string
    2.15 -  val mode_markup: Markup.T -> string * string
    2.16 -  val add_mode: string -> (string -> int -> string) -> (Markup.T -> string * string) -> unit
    2.17 +  val default_indent: string -> int -> output
    2.18 +  val default_markup: Markup.T -> output * output
    2.19 +  val mode_markup: Markup.T -> output * output
    2.20 +  val add_mode: string -> (string -> int -> output) -> (Markup.T -> output * output) -> unit
    2.21    type T
    2.22 -  val raw_str: string * int -> T
    2.23 +  val raw_str: output * int -> T
    2.24    val str: string -> T
    2.25    val brk: int -> T
    2.26    val fbrk: T
    2.27 @@ -63,7 +63,7 @@
    2.28    val pprint: T -> pprint_args -> unit
    2.29    val symbolicN: string
    2.30    val output_buffer: T -> Buffer.T
    2.31 -  val output: T -> string
    2.32 +  val output: T -> output
    2.33    val string_of: T -> string
    2.34    val str_of: T -> string
    2.35    val writeln: T -> unit
    2.36 @@ -118,7 +118,7 @@
    2.37  
    2.38  datatype T =
    2.39    Block of Markup.T * T list * int * int |  (*markup, body, indentation, length*)
    2.40 -  String of string * int |                  (*text, length*)
    2.41 +  String of output * int |                  (*text, length*)
    2.42    Break of bool * int;                      (*mandatory flag, width if not taken*)
    2.43  
    2.44  fun length (Block (_, _, _, len)) = len

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

     4.1 --- a/src/Pure/Syntax/printer.ML	Sun Jul 08 19:52:10 2007 +0200
     4.2 +++ b/src/Pure/Syntax/printer.ML	Mon Jul 09 11:44:20 2007 +0200
     4.3 @@ -31,10 +31,10 @@
     4.4    val merge_prtabs: prtabs -> prtabs -> prtabs
     4.5    val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
     4.6      -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
     4.7 -    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T list
     4.8 +    -> (string -> (string -> output * int) option) -> Ast.ast -> Pretty.T list
     4.9    val pretty_typ_ast: Proof.context -> bool -> prtabs
    4.10      -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
    4.11 -    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T list
    4.12 +    -> (string -> (string -> output * int) option) -> Ast.ast -> Pretty.T list
    4.13  end;
    4.14  
    4.15  structure Printer: PRINTER =

     5.1 --- a/src/Pure/Syntax/syn_ext.ML	Sun Jul 08 19:52:10 2007 +0200
     5.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Jul 09 11:44:20 2007 +0200
     5.3 @@ -14,8 +14,8 @@
     5.4    val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
     5.5    val mk_trfun: string * 'a -> string * ('a * stamp)
     5.6    val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
     5.7 -  val tokentrans_mode: string -> (string * (string -> string * int)) list ->
     5.8 -    (string * string * (string -> string * int)) list
     5.9 +  val tokentrans_mode: string -> (string * (string -> output * int)) list ->
    5.10 +    (string * string * (string -> output * int)) list
    5.11    val standard_token_classes: string list
    5.12  end;
    5.13  
    5.14 @@ -49,7 +49,7 @@
    5.15          (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    5.16        print_rules: (Ast.ast * Ast.ast) list,
    5.17        print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.18 -      token_translation: (string * string * (string -> string * int)) list}
    5.19 +      token_translation: (string * string * (string -> output * int)) list}
    5.20    val mfix_delims: string -> string list
    5.21    val mfix_args: string -> int
    5.22    val escape_mfix: string -> string
    5.23 @@ -59,14 +59,14 @@
    5.24      (string * ((Proof.context -> term list -> term) * stamp)) list *
    5.25      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    5.26      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
    5.27 -    -> (string * string * (string -> string * int)) list
    5.28 +    -> (string * string * (string -> output * int)) list
    5.29      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    5.30    val syn_ext: mfix list -> string list ->
    5.31      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.32      (string * ((Proof.context -> term list -> term) * stamp)) list *
    5.33      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    5.34      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
    5.35 -    -> (string * string * (string -> string * int)) list
    5.36 +    -> (string * string * (string -> output * int)) list
    5.37      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    5.38    val syn_ext_const_names: string list -> syn_ext
    5.39    val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    5.40 @@ -80,7 +80,7 @@
    5.41      (string * ((Proof.context -> term list -> term) * stamp)) list *
    5.42      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    5.43      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    5.44 -  val syn_ext_tokentrfuns: (string * string * (string -> string * int)) list -> syn_ext
    5.45 +  val syn_ext_tokentrfuns: (string * string * (string -> output * int)) list -> syn_ext
    5.46    val standard_token_markers: string list
    5.47    val pure_ext: syn_ext
    5.48  end;
    5.49 @@ -343,7 +343,7 @@
    5.50        (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    5.51      print_rules: (Ast.ast * Ast.ast) list,
    5.52      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.53 -    token_translation: (string * string * (string -> string * int)) list};
    5.54 +    token_translation: (string * string * (string -> output * int)) list};
    5.55  
    5.56  
    5.57  (* syn_ext *)

     6.1 --- a/src/Pure/Syntax/syntax.ML	Sun Jul 08 19:52:10 2007 +0200
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Jul 09 11:44:20 2007 +0200
     6.3 @@ -55,7 +55,7 @@
     6.4      (string * ((Proof.context -> term list -> term) * stamp)) list *
     6.5      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     6.6      (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
     6.7 -  val extend_tokentrfuns: (string * string * (string -> string * int)) list -> syntax -> syntax
     6.8 +  val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax
     6.9    val remove_const_gram: (string -> bool) ->
    6.10      mode -> (string * typ * mixfix) list -> syntax -> syntax
    6.11    val extend_trrules: Proof.context -> (string -> bool) -> syntax ->
    6.12 @@ -183,7 +183,7 @@
    6.13      print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
    6.14      print_ruletab: ruletab,
    6.15      print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    6.16 -    tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
    6.17 +    tokentrtab: (string * (string * ((string -> output * int) * stamp)) list) list,
    6.18      prtabs: Printer.prtabs} * stamp;
    6.19  
    6.20  fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;

     7.1 --- a/src/Pure/sign.ML	Sun Jul 08 19:52:10 2007 +0200
     7.2 +++ b/src/Pure/sign.ML	Mon Jul 09 11:44:20 2007 +0200
     7.3 @@ -38,8 +38,8 @@
     7.4    val add_advanced_trfunsT:
     7.5      (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
     7.6    val add_tokentrfuns:
     7.7 -    (string * string * (string -> string * int)) list -> theory -> theory
     7.8 -  val add_mode_tokentrfuns: string -> (string * (string -> string * int)) list
     7.9 +    (string * string * (string -> output * int)) list -> theory -> theory
    7.10 +  val add_mode_tokentrfuns: string -> (string * (string -> output * int)) list
    7.11      -> theory -> theory
    7.12    val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    7.13    val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory