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 @