token translation: real;
authorwenzelm
Tue Mar 09 12:11:29 1999 +0100 (1999-03-09)
changeset 63227047300264c9
parent 6321 207f518167e8
child 6323 e5b3e46d5dbd
token translation: real;
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/token_trans.ML
     1.1 --- a/src/Pure/Syntax/printer.ML	Tue Mar 09 12:11:00 1999 +0100
     1.2 +++ b/src/Pure/Syntax/printer.ML	Tue Mar 09 12:11:29 1999 +0100
     1.3 @@ -25,10 +25,10 @@
     1.4    val merge_prtabs: prtabs -> prtabs -> prtabs
     1.5    val pretty_term_ast: bool -> prtabs
     1.6      -> (string -> (Ast.ast list -> Ast.ast) list)
     1.7 -    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T
     1.8 +    -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
     1.9    val pretty_typ_ast: bool -> prtabs
    1.10      -> (string -> (Ast.ast list -> Ast.ast) list)
    1.11 -    -> (string -> (string -> string * int) option) -> Ast.ast -> Pretty.T
    1.12 +    -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
    1.13  end;
    1.14  
    1.15  structure Printer: PRINTER =
    1.16 @@ -330,7 +330,7 @@
    1.17                else prnt (prnps, tbs);
    1.18        in
    1.19          (case token_trans a args of     (*try token translation function*)
    1.20 -          Some (s, len) => [Pretty.strlen s len]	(* FIXME Pretty.sym (!?) *)
    1.21 +          Some (s, len) => [Pretty.strlen_real s len]
    1.22          | None =>			(*try print translation functions*)
    1.23              astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
    1.24        end
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Mar 09 12:11:00 1999 +0100
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Mar 09 12:11:29 1999 +0100
     2.3 @@ -42,18 +42,18 @@
     2.4        print_translation: (string * (bool -> typ -> term list -> term)) list,
     2.5        print_rules: (Ast.ast * Ast.ast) list,
     2.6        print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
     2.7 -      token_translation: (string * string * (string -> string * int)) list}
     2.8 +      token_translation: (string * string * (string -> string * real)) list}
     2.9    val mfix_args: string -> int
    2.10    val mk_syn_ext: bool -> string list -> mfix list ->
    2.11      string list -> (string * (Ast.ast list -> Ast.ast)) list *
    2.12      (string * (term list -> term)) list *
    2.13      (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    2.14 -    -> (string * string * (string -> string * int)) list
    2.15 +    -> (string * string * (string -> string * real)) list
    2.16      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.17    val syn_ext: string list -> mfix list -> string list ->
    2.18      (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    2.19      (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    2.20 -    -> (string * string * (string -> string * int)) list
    2.21 +    -> (string * string * (string -> string * real)) list
    2.22      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.23    val syn_ext_logtypes: string list -> syn_ext
    2.24    val syn_ext_const_names: string list -> string list -> syn_ext
    2.25 @@ -66,7 +66,7 @@
    2.26    val syn_ext_trfunsT: string list ->
    2.27      (string * (bool -> typ -> term list -> term)) list -> syn_ext
    2.28    val syn_ext_tokentrfuns: string list
    2.29 -    -> (string * string * (string -> string * int)) list -> syn_ext
    2.30 +    -> (string * string * (string -> string * real)) list -> syn_ext
    2.31    val pure_ext: syn_ext
    2.32  end;
    2.33  
    2.34 @@ -293,7 +293,7 @@
    2.35      print_translation: (string * (bool -> typ -> term list -> term)) list,
    2.36      print_rules: (Ast.ast * Ast.ast) list,
    2.37      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    2.38 -    token_translation: (string * string * (string -> string * int)) list}
    2.39 +    token_translation: (string * string * (string -> string * real)) list}
    2.40  
    2.41  
    2.42  (* syn_ext *)
     3.1 --- a/src/Pure/Syntax/syntax.ML	Tue Mar 09 12:11:00 1999 +0100
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Mar 09 12:11:29 1999 +0100
     3.3 @@ -15,6 +15,7 @@
     3.4  
     3.5  signature SYNTAX =
     3.6  sig
     3.7 +  include TOKEN_TRANS0
     3.8    include AST1
     3.9    include LEXICON0
    3.10    include SYN_EXT0
    3.11 @@ -37,7 +38,7 @@
    3.12      (string * (term list -> term)) list *
    3.13      (string * (ast list -> ast)) list -> syntax
    3.14    val extend_trfunsT: syntax -> (string * (bool -> typ -> term list -> term)) list -> syntax
    3.15 -  val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax
    3.16 +  val extend_tokentrfuns: syntax -> (string * string * (string -> string * real)) list -> syntax
    3.17    val extend_trrules: syntax -> (string * string) trrule list -> syntax
    3.18    val extend_trrules_i: syntax -> ast trrule list -> syntax
    3.19    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    3.20 @@ -174,7 +175,7 @@
    3.21      print_trtab: ((bool -> typ -> term list -> term) * stamp) list Symtab.table,
    3.22      print_ruletab: ruletab,
    3.23      print_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    3.24 -    tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
    3.25 +    tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
    3.26      prtabs: Printer.prtabs}
    3.27  
    3.28  
    3.29 @@ -499,7 +500,7 @@
    3.30  
    3.31  (** export parts of internal Syntax structures **)
    3.32  
    3.33 -open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    3.34 +open TokenTrans Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    3.35  
    3.36  
    3.37  end;
     4.1 --- a/src/Pure/Syntax/token_trans.ML	Tue Mar 09 12:11:00 1999 +0100
     4.2 +++ b/src/Pure/Syntax/token_trans.ML	Tue Mar 09 12:11:29 1999 +0100
     4.3 @@ -3,10 +3,19 @@
     4.4      Author:     Markus Wenzel, TU Muenchen
     4.5  
     4.6  Token translations for xterm, emacs and latex output.
     4.7 +
     4.8 +TODO:
     4.9 +  - elim this file, move stuff to individual print/presentation modes (!?);
    4.10  *)
    4.11  
    4.12 +signature TOKEN_TRANS0 =
    4.13 +sig
    4.14 +  val standard_token_classes: string list
    4.15 +end;
    4.16 +
    4.17  signature TOKEN_TRANS =
    4.18  sig
    4.19 +  include TOKEN_TRANS0
    4.20    val normal: string
    4.21    val bold: string
    4.22    val underline: string
    4.23 @@ -31,7 +40,7 @@
    4.24    val xterm_color_free: string ref
    4.25    val xterm_color_bound: string ref
    4.26    val xterm_color_var: string ref
    4.27 -  val token_translation: (string * string * (string -> string * int)) list
    4.28 +  val token_translation: (string * string * (string -> string * real)) list
    4.29  end;
    4.30  
    4.31  structure TokenTrans: TOKEN_TRANS =
    4.32 @@ -42,7 +51,8 @@
    4.33  
    4.34  fun trans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
    4.35  
    4.36 -val std_token_classes = ["class", "tfree", "tvar", "free", "bound", "var"];
    4.37 +val standard_token_classes =
    4.38 +  ["class", "tfree", "tvar", "free", "bound", "var", "xnum", "xstr"];
    4.39  
    4.40  
    4.41  
    4.42 @@ -64,7 +74,7 @@
    4.43  val cyan = "\^[[36m";
    4.44  val white = "\^[[37m";
    4.45  
    4.46 -fun style (ref s) x = (s ^ x ^ normal, size x);
    4.47 +fun style (ref s) x = (s ^ x ^ normal, real (size x));
    4.48  
    4.49  
    4.50  (* print modes "xterm" and "xterm_color" *)
    4.51 @@ -113,7 +123,7 @@
    4.52  val bound_tag = "\^A5";
    4.53  val var_tag = "\^A6";
    4.54  
    4.55 -fun tagit p x = (p ^ x ^ end_tag, size x);
    4.56 +fun tagit p x = (p ^ x ^ end_tag, real (size x));
    4.57  
    4.58  in
    4.59  
    4.60 @@ -142,7 +152,7 @@
    4.61  val bound_tag = oct_char "355";
    4.62  val var_tag = oct_char "356";
    4.63  
    4.64 -fun tagit p x = (p ^ x ^ end_tag, size x);
    4.65 +fun tagit p x = (p ^ x ^ end_tag, real (size x));
    4.66  
    4.67  in
    4.68  
    4.69 @@ -164,14 +174,14 @@
    4.70  (* FIXME 'a -> \alpha etc. *)
    4.71  
    4.72  val latex_trans =
    4.73 - trans_mode "latex" [] : (string * string * (string -> string * int)) list;
    4.74 + trans_mode "latex" [] : (string * string * (string -> string * real)) list;
    4.75  
    4.76  
    4.77  
    4.78  (** standard token translations **)
    4.79  
    4.80  val token_translation =
    4.81 -  map (fn s => ("", s, fn x => (x, size x))) std_token_classes @
    4.82 +  map (fn s => ("", s, fn x => (x, real (size x)))) standard_token_classes @
    4.83    xterm_trans @
    4.84    emacs_trans @
    4.85    proof_general_trans @