author | wenzelm |
Sat, 25 Mar 2000 12:59:31 +0100 | |
changeset 8575 | 7d79d2473b5e |
parent 6695 | d3ba5427d562 |
child 11697 | 8dd899efbd35 |
permissions | -rw-r--r-- |
2697 | 1 |
(* Title: Pure/Syntax/token_trans.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
5 |
Token translations for xterm output. |
2697 | 6 |
*) |
7 |
||
6322 | 8 |
signature TOKEN_TRANS0 = |
9 |
sig |
|
10 |
val standard_token_classes: string list |
|
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
11 |
val tokentrans_mode: string -> (string * (string -> string * real)) list -> |
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
12 |
(string * string * (string -> string * real)) list |
6322 | 13 |
end; |
14 |
||
2697 | 15 |
signature TOKEN_TRANS = |
16 |
sig |
|
6322 | 17 |
include TOKEN_TRANS0 |
2707 | 18 |
val normal: string |
19 |
val bold: string |
|
20 |
val underline: string |
|
21 |
val reverse: string |
|
22 |
val black: string |
|
23 |
val red: string |
|
24 |
val green: string |
|
25 |
val yellow: string |
|
26 |
val blue: string |
|
27 |
val purple: string |
|
28 |
val cyan: string |
|
29 |
val white: string |
|
2710 | 30 |
val xterm_class: string ref |
31 |
val xterm_tfree: string ref |
|
32 |
val xterm_tvar: string ref |
|
33 |
val xterm_free: string ref |
|
34 |
val xterm_bound: string ref |
|
35 |
val xterm_var: string ref |
|
36 |
val xterm_color_class: string ref |
|
37 |
val xterm_color_tfree: string ref |
|
38 |
val xterm_color_tvar: string ref |
|
39 |
val xterm_color_free: string ref |
|
40 |
val xterm_color_bound: string ref |
|
41 |
val xterm_color_var: string ref |
|
6322 | 42 |
val token_translation: (string * string * (string -> string * real)) list |
2697 | 43 |
end; |
44 |
||
45 |
structure TokenTrans: TOKEN_TRANS = |
|
46 |
struct |
|
47 |
||
5406 | 48 |
|
2697 | 49 |
(** misc utils **) |
50 |
||
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
51 |
fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs; |
2697 | 52 |
|
6322 | 53 |
val standard_token_classes = |
54 |
["class", "tfree", "tvar", "free", "bound", "var", "xnum", "xstr"]; |
|
2697 | 55 |
|
56 |
||
57 |
||
58 |
(** xterm output **) |
|
59 |
||
60 |
(* styles *) |
|
61 |
||
62 |
val normal = "\^[[0m"; |
|
63 |
val bold = "\^[[1m"; |
|
64 |
val underline = "\^[[4m"; |
|
2707 | 65 |
val reverse = "\^[[7m"; |
66 |
||
2710 | 67 |
val black = "\^[[30m"; |
68 |
val red = "\^[[31m"; |
|
69 |
val green = "\^[[32m"; |
|
2707 | 70 |
val yellow = "\^[[33m"; |
2710 | 71 |
val blue = "\^[[34m"; |
72 |
val purple = "\^[[35m"; |
|
2707 | 73 |
val cyan = "\^[[36m"; |
74 |
val white = "\^[[37m"; |
|
2697 | 75 |
|
6322 | 76 |
fun style (ref s) x = (s ^ x ^ normal, real (size x)); |
2710 | 77 |
|
78 |
||
79 |
(* print modes "xterm" and "xterm_color" *) |
|
2707 | 80 |
|
2710 | 81 |
val xterm_class = ref normal; |
82 |
val xterm_tfree = ref bold; |
|
83 |
val xterm_tvar = ref bold; |
|
84 |
val xterm_free = ref bold; |
|
85 |
val xterm_bound = ref underline; |
|
86 |
val xterm_var = ref bold; |
|
2697 | 87 |
|
2710 | 88 |
val xterm_color_class = ref red; |
89 |
val xterm_color_tfree = ref purple; |
|
90 |
val xterm_color_tvar = ref purple; |
|
91 |
val xterm_color_free = ref blue; |
|
92 |
val xterm_color_bound = ref green; |
|
93 |
val xterm_color_var = ref blue; |
|
2697 | 94 |
|
95 |
val xterm_trans = |
|
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
96 |
tokentrans_mode "xterm" |
2710 | 97 |
[("class", style xterm_class), |
98 |
("tfree", style xterm_tfree), |
|
99 |
("tvar", style xterm_tvar), |
|
100 |
("free", style xterm_free), |
|
101 |
("bound", style xterm_bound), |
|
102 |
("var", style xterm_var)] @ |
|
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
103 |
tokentrans_mode "xterm_color" |
2710 | 104 |
[("class", style xterm_color_class), |
105 |
("tfree", style xterm_color_tfree), |
|
106 |
("tvar", style xterm_color_tvar), |
|
107 |
("free", style xterm_color_free), |
|
108 |
("bound", style xterm_color_bound), |
|
109 |
("var", style xterm_color_var)]; |
|
2697 | 110 |
|
111 |
||
5406 | 112 |
|
113 |
(** standard token translations **) |
|
2697 | 114 |
|
115 |
val token_translation = |
|
6322 | 116 |
map (fn s => ("", s, fn x => (x, real (size x)))) standard_token_classes @ |
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
117 |
xterm_trans; |
2697 | 118 |
|
119 |
||
120 |
end; |