2697
|
1 |
(* Title: Pure/Syntax/token_trans.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
5406
|
5 |
Token translations for xterm, emacs and latex output.
|
2697
|
6 |
*)
|
|
7 |
|
|
8 |
signature TOKEN_TRANS =
|
|
9 |
sig
|
2707
|
10 |
val normal: string
|
|
11 |
val bold: string
|
|
12 |
val underline: string
|
|
13 |
val reverse: string
|
|
14 |
val black: string
|
|
15 |
val red: string
|
|
16 |
val green: string
|
|
17 |
val yellow: string
|
|
18 |
val blue: string
|
|
19 |
val purple: string
|
|
20 |
val cyan: string
|
|
21 |
val white: string
|
2710
|
22 |
val xterm_class: string ref
|
|
23 |
val xterm_tfree: string ref
|
|
24 |
val xterm_tvar: string ref
|
|
25 |
val xterm_free: string ref
|
|
26 |
val xterm_bound: string ref
|
|
27 |
val xterm_var: string ref
|
|
28 |
val xterm_color_class: string ref
|
|
29 |
val xterm_color_tfree: string ref
|
|
30 |
val xterm_color_tvar: string ref
|
|
31 |
val xterm_color_free: string ref
|
|
32 |
val xterm_color_bound: string ref
|
|
33 |
val xterm_color_var: string ref
|
|
34 |
val token_translation: (string * string * (string -> string * int)) list
|
2697
|
35 |
end;
|
|
36 |
|
|
37 |
structure TokenTrans: TOKEN_TRANS =
|
|
38 |
struct
|
|
39 |
|
5406
|
40 |
|
2697
|
41 |
(** misc utils **)
|
|
42 |
|
|
43 |
fun trans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
|
|
44 |
|
5406
|
45 |
val std_token_classes = ["class", "tfree", "tvar", "free", "bound", "var"];
|
2697
|
46 |
|
|
47 |
|
|
48 |
|
|
49 |
(** xterm output **)
|
|
50 |
|
|
51 |
(* styles *)
|
|
52 |
|
|
53 |
val normal = "\^[[0m";
|
|
54 |
val bold = "\^[[1m";
|
|
55 |
val underline = "\^[[4m";
|
2707
|
56 |
val reverse = "\^[[7m";
|
|
57 |
|
2710
|
58 |
val black = "\^[[30m";
|
|
59 |
val red = "\^[[31m";
|
|
60 |
val green = "\^[[32m";
|
2707
|
61 |
val yellow = "\^[[33m";
|
2710
|
62 |
val blue = "\^[[34m";
|
|
63 |
val purple = "\^[[35m";
|
2707
|
64 |
val cyan = "\^[[36m";
|
|
65 |
val white = "\^[[37m";
|
2697
|
66 |
|
2710
|
67 |
fun style (ref s) x = (s ^ x ^ normal, size x);
|
|
68 |
|
|
69 |
|
|
70 |
(* print modes "xterm" and "xterm_color" *)
|
2707
|
71 |
|
2710
|
72 |
val xterm_class = ref normal;
|
|
73 |
val xterm_tfree = ref bold;
|
|
74 |
val xterm_tvar = ref bold;
|
|
75 |
val xterm_free = ref bold;
|
|
76 |
val xterm_bound = ref underline;
|
|
77 |
val xterm_var = ref bold;
|
2697
|
78 |
|
2710
|
79 |
val xterm_color_class = ref red;
|
|
80 |
val xterm_color_tfree = ref purple;
|
|
81 |
val xterm_color_tvar = ref purple;
|
|
82 |
val xterm_color_free = ref blue;
|
|
83 |
val xterm_color_bound = ref green;
|
|
84 |
val xterm_color_var = ref blue;
|
2697
|
85 |
|
|
86 |
val xterm_trans =
|
|
87 |
trans_mode "xterm"
|
2710
|
88 |
[("class", style xterm_class),
|
|
89 |
("tfree", style xterm_tfree),
|
|
90 |
("tvar", style xterm_tvar),
|
|
91 |
("free", style xterm_free),
|
|
92 |
("bound", style xterm_bound),
|
|
93 |
("var", style xterm_var)] @
|
|
94 |
trans_mode "xterm_color"
|
|
95 |
[("class", style xterm_color_class),
|
|
96 |
("tfree", style xterm_color_tfree),
|
|
97 |
("tvar", style xterm_color_tvar),
|
|
98 |
("free", style xterm_color_free),
|
|
99 |
("bound", style xterm_color_bound),
|
|
100 |
("var", style xterm_color_var)];
|
2697
|
101 |
|
|
102 |
|
5406
|
103 |
|
|
104 |
(** emacs output (Isamode) **)
|
|
105 |
|
|
106 |
(* tags *)
|
|
107 |
|
|
108 |
val end_tag = "\^A0";
|
|
109 |
val tclass_tag = "\^A1";
|
|
110 |
val tfree_tag = "\^A2";
|
|
111 |
val tvar_tag = "\^A3";
|
|
112 |
val free_tag = "\^A4";
|
|
113 |
val bound_tag = "\^A5";
|
|
114 |
val var_tag = "\^A6";
|
|
115 |
|
|
116 |
fun tagit p x = (p ^ x ^ end_tag, size x);
|
|
117 |
|
|
118 |
|
|
119 |
(* print mode "emacs" *)
|
|
120 |
|
|
121 |
val emacs_trans =
|
|
122 |
trans_mode "emacs"
|
|
123 |
[("class", tagit tclass_tag),
|
|
124 |
("tfree", tagit tfree_tag),
|
|
125 |
("tvar", tagit tvar_tag),
|
|
126 |
("free", tagit free_tag),
|
|
127 |
("bound", tagit bound_tag),
|
|
128 |
("var", tagit var_tag)];
|
|
129 |
|
|
130 |
|
|
131 |
|
2697
|
132 |
(** LaTeX output **)
|
|
133 |
|
|
134 |
(* FIXME 'a -> \alpha etc. *)
|
|
135 |
|
5406
|
136 |
val latex_trans =
|
5408
|
137 |
trans_mode "latex" [] : (string * string * (string -> string * int)) list;
|
2697
|
138 |
|
5406
|
139 |
|
|
140 |
|
|
141 |
(** standard token translations **)
|
2697
|
142 |
|
|
143 |
val token_translation =
|
5406
|
144 |
map (fn s => ("", s, fn x => (x, size x))) std_token_classes @
|
|
145 |
xterm_trans @
|
|
146 |
emacs_trans @
|
|
147 |
latex_trans;
|
2697
|
148 |
|
|
149 |
|
|
150 |
end;
|