# HG changeset patch
# User wenzelm
# Date 920977889 -3600
# Node ID 7047300264c9c29ef19b5ece1f78722a9d9a283b
# Parent  207f518167e884f2541f0a80ccc3961ae386b801
token translation: real;

diff -r 207f518167e8 -r 7047300264c9 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue Mar 09 12:11:00 1999 +0100
+++ b/src/Pure/Syntax/printer.ML	Tue Mar 09 12:11:29 1999 +0100
@@ -25,10 +25,10 @@
   val merge_prtabs: prtabs -> prtabs -> prtabs
   val pretty_term_ast: bool -> prtabs
     -> (string -> (Ast.ast list -> Ast.ast) list)
-    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T
+    -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
   val pretty_typ_ast: bool -> prtabs
     -> (string -> (Ast.ast list -> Ast.ast) list)
-    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T
+    -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
 end;
 
 structure Printer: PRINTER =
@@ -330,7 +330,7 @@
               else prnt (prnps, tbs);
       in
         (case token_trans a args of     (*try token translation function*)
-          Some (s, len) => [Pretty.strlen s len]	(* FIXME Pretty.sym (!?) *)
+          Some (s, len) => [Pretty.strlen_real s len]
         | None =>			(*try print translation functions*)
             astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
       end
diff -r 207f518167e8 -r 7047300264c9 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Tue Mar 09 12:11:00 1999 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Tue Mar 09 12:11:29 1999 +0100
@@ -42,18 +42,18 @@
       print_translation: (string * (bool -> typ -> term list -> term)) list,
       print_rules: (Ast.ast * Ast.ast) list,
       print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
-      token_translation: (string * string * (string -> string * int)) list}
+      token_translation: (string * string * (string -> string * real)) list}
   val mfix_args: string -> int
   val mk_syn_ext: bool -> string list -> mfix list ->
     string list -> (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
     (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
-    -> (string * string * (string -> string * int)) list
+    -> (string * string * (string -> string * real)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext: string list -> mfix list -> string list ->
     (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
     (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
-    -> (string * string * (string -> string * int)) list
+    -> (string * string * (string -> string * real)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_logtypes: string list -> syn_ext
   val syn_ext_const_names: string list -> string list -> syn_ext
@@ -66,7 +66,7 @@
   val syn_ext_trfunsT: string list ->
     (string * (bool -> typ -> term list -> term)) list -> syn_ext
   val syn_ext_tokentrfuns: string list
-    -> (string * string * (string -> string * int)) list -> syn_ext
+    -> (string * string * (string -> string * real)) list -> syn_ext
   val pure_ext: syn_ext
 end;
 
@@ -293,7 +293,7 @@
     print_translation: (string * (bool -> typ -> term list -> term)) list,
     print_rules: (Ast.ast * Ast.ast) list,
     print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
-    token_translation: (string * string * (string -> string * int)) list}
+    token_translation: (string * string * (string -> string * real)) list}
 
 
 (* syn_ext *)
diff -r 207f518167e8 -r 7047300264c9 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Mar 09 12:11:00 1999 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 09 12:11:29 1999 +0100
@@ -15,6 +15,7 @@
 
 signature SYNTAX =
 sig
+  include TOKEN_TRANS0
   include AST1
   include LEXICON0
   include SYN_EXT0
@@ -37,7 +38,7 @@
     (string * (term list -> term)) list *
     (string * (ast list -> ast)) list -> syntax
   val extend_trfunsT: syntax -> (string * (bool -> typ -> term list -> term)) list -> syntax
-  val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax
+  val extend_tokentrfuns: syntax -> (string * string * (string -> string * real)) list -> syntax
   val extend_trrules: syntax -> (string * string) trrule list -> syntax
   val extend_trrules_i: syntax -> ast trrule list -> syntax
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
@@ -174,7 +175,7 @@
     print_trtab: ((bool -> typ -> term list -> term) * stamp) list Symtab.table,
     print_ruletab: ruletab,
     print_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
-    tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
+    tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
     prtabs: Printer.prtabs}
 
 
@@ -499,7 +500,7 @@
 
 (** export parts of internal Syntax structures **)
 
-open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
+open TokenTrans Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
 
 
 end;
diff -r 207f518167e8 -r 7047300264c9 src/Pure/Syntax/token_trans.ML
--- a/src/Pure/Syntax/token_trans.ML	Tue Mar 09 12:11:00 1999 +0100
+++ b/src/Pure/Syntax/token_trans.ML	Tue Mar 09 12:11:29 1999 +0100
@@ -3,10 +3,19 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Token translations for xterm, emacs and latex output.
+
+TODO:
+  - elim this file, move stuff to individual print/presentation modes (!?);
 *)
 
+signature TOKEN_TRANS0 =
+sig
+  val standard_token_classes: string list
+end;
+
 signature TOKEN_TRANS =
 sig
+  include TOKEN_TRANS0
   val normal: string
   val bold: string
   val underline: string
@@ -31,7 +40,7 @@
   val xterm_color_free: string ref
   val xterm_color_bound: string ref
   val xterm_color_var: string ref
-  val token_translation: (string * string * (string -> string * int)) list
+  val token_translation: (string * string * (string -> string * real)) list
 end;
 
 structure TokenTrans: TOKEN_TRANS =
@@ -42,7 +51,8 @@
 
 fun trans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
 
-val std_token_classes = ["class", "tfree", "tvar", "free", "bound", "var"];
+val standard_token_classes =
+  ["class", "tfree", "tvar", "free", "bound", "var", "xnum", "xstr"];
 
 
 
@@ -64,7 +74,7 @@
 val cyan = "\^[[36m";
 val white = "\^[[37m";
 
-fun style (ref s) x = (s ^ x ^ normal, size x);
+fun style (ref s) x = (s ^ x ^ normal, real (size x));
 
 
 (* print modes "xterm" and "xterm_color" *)
@@ -113,7 +123,7 @@
 val bound_tag = "\^A5";
 val var_tag = "\^A6";
 
-fun tagit p x = (p ^ x ^ end_tag, size x);
+fun tagit p x = (p ^ x ^ end_tag, real (size x));
 
 in
 
@@ -142,7 +152,7 @@
 val bound_tag = oct_char "355";
 val var_tag = oct_char "356";
 
-fun tagit p x = (p ^ x ^ end_tag, size x);
+fun tagit p x = (p ^ x ^ end_tag, real (size x));
 
 in
 
@@ -164,14 +174,14 @@
 (* FIXME 'a -> \alpha etc. *)
 
 val latex_trans =
- trans_mode "latex" [] : (string * string * (string -> string * int)) list;
+ trans_mode "latex" [] : (string * string * (string -> string * real)) list;
 
 
 
 (** standard token translations **)
 
 val token_translation =
-  map (fn s => ("", s, fn x => (x, size x))) std_token_classes @
+  map (fn s => ("", s, fn x => (x, real (size x)))) standard_token_classes @
   xterm_trans @
   emacs_trans @
   proof_general_trans @