author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14880 | 7586233bd4bd |
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 |
11795 | 18 |
val standard_token_markers: string list |
2707 | 19 |
val normal: string |
20 |
val bold: string |
|
21 |
val underline: string |
|
22 |
val reverse: string |
|
23 |
val black: string |
|
24 |
val red: string |
|
25 |
val green: string |
|
26 |
val yellow: string |
|
27 |
val blue: string |
|
28 |
val purple: string |
|
29 |
val cyan: string |
|
30 |
val white: string |
|
2710 | 31 |
val xterm_class: string ref |
32 |
val xterm_tfree: string ref |
|
33 |
val xterm_tvar: string ref |
|
34 |
val xterm_free: string ref |
|
35 |
val xterm_bound: string ref |
|
36 |
val xterm_var: string ref |
|
37 |
val xterm_color_class: string ref |
|
38 |
val xterm_color_tfree: string ref |
|
39 |
val xterm_color_tvar: string ref |
|
40 |
val xterm_color_free: string ref |
|
41 |
val xterm_color_bound: string ref |
|
42 |
val xterm_color_var: string ref |
|
6322 | 43 |
val token_translation: (string * string * (string -> string * real)) list |
2697 | 44 |
end; |
45 |
||
46 |
structure TokenTrans: TOKEN_TRANS = |
|
47 |
struct |
|
48 |
||
5406 | 49 |
|
2697 | 50 |
(** misc utils **) |
51 |
||
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
52 |
fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs; |
2697 | 53 |
|
6322 | 54 |
val standard_token_classes = |
11697 | 55 |
["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"]; |
2697 | 56 |
|
11795 | 57 |
val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes; |
2697 | 58 |
|
59 |
||
60 |
(** xterm output **) |
|
61 |
||
62 |
(* styles *) |
|
63 |
||
64 |
val normal = "\^[[0m"; |
|
65 |
val bold = "\^[[1m"; |
|
66 |
val underline = "\^[[4m"; |
|
2707 | 67 |
val reverse = "\^[[7m"; |
68 |
||
2710 | 69 |
val black = "\^[[30m"; |
70 |
val red = "\^[[31m"; |
|
71 |
val green = "\^[[32m"; |
|
2707 | 72 |
val yellow = "\^[[33m"; |
2710 | 73 |
val blue = "\^[[34m"; |
74 |
val purple = "\^[[35m"; |
|
2707 | 75 |
val cyan = "\^[[36m"; |
76 |
val white = "\^[[37m"; |
|
2697 | 77 |
|
14880 | 78 |
fun style (ref s) x = Output.output_width x |> apfst (enclose s normal); |
2710 | 79 |
|
80 |
||
81 |
(* print modes "xterm" and "xterm_color" *) |
|
2707 | 82 |
|
2710 | 83 |
val xterm_class = ref normal; |
84 |
val xterm_tfree = ref bold; |
|
85 |
val xterm_tvar = ref bold; |
|
86 |
val xterm_free = ref bold; |
|
87 |
val xterm_bound = ref underline; |
|
88 |
val xterm_var = ref bold; |
|
2697 | 89 |
|
2710 | 90 |
val xterm_color_class = ref red; |
91 |
val xterm_color_tfree = ref purple; |
|
92 |
val xterm_color_tvar = ref purple; |
|
93 |
val xterm_color_free = ref blue; |
|
94 |
val xterm_color_bound = ref green; |
|
95 |
val xterm_color_var = ref blue; |
|
2697 | 96 |
|
97 |
val xterm_trans = |
|
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
98 |
tokentrans_mode "xterm" |
2710 | 99 |
[("class", style xterm_class), |
100 |
("tfree", style xterm_tfree), |
|
101 |
("tvar", style xterm_tvar), |
|
102 |
("free", style xterm_free), |
|
103 |
("bound", style xterm_bound), |
|
104 |
("var", style xterm_var)] @ |
|
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
105 |
tokentrans_mode "xterm_color" |
2710 | 106 |
[("class", style xterm_color_class), |
107 |
("tfree", style xterm_color_tfree), |
|
108 |
("tvar", style xterm_color_tvar), |
|
109 |
("free", style xterm_color_free), |
|
110 |
("bound", style xterm_color_bound), |
|
111 |
("var", style xterm_color_var)]; |
|
2697 | 112 |
|
113 |
||
5406 | 114 |
|
115 |
(** standard token translations **) |
|
2697 | 116 |
|
117 |
val token_translation = |
|
14880 | 118 |
map (fn s => ("", s, Output.output_width)) standard_token_classes @ |
6695
d3ba5427d562
Isamode and ProofGeneral configuration moved to Pure/Interface;
wenzelm
parents:
6322
diff
changeset
|
119 |
xterm_trans; |
2697 | 120 |
|
121 |
||
122 |
end; |