author | paulson |
Tue, 05 Sep 2000 10:16:03 +0200 | |
changeset 9841 | ca3173f87b5c |
parent 6026 | 649b98cf9bc3 |
permissions | -rw-r--r-- |
1826 | 1 |
/* |
2 |
* translation table for the low-8-bit ascii codes |
|
3 |
* translation takes place only if destCode is TO_LaTeX |
|
4 |
* |
|
5 |
* the row number + START_LOW_TABLE -1 is the ascii code !! |
|
6 |
*/ |
|
7 |
||
8 |
/* do not edit the lines between BEGIN_OF_LOW_TABLE and END_OF_LOW_TABLE */ |
|
9 |
/* these lines are automatically generated by gen-isa2latex */ |
|
10 |
||
11 |
/* BEGIN_OF_LOW_TABLE */ |
|
12 |
char *translationTableLow[END_LOW_TABLE - START_LOW_TABLE + 1] = { |
|
13 |
"\\ ", |
|
14 |
"!", |
|
15 |
"\x22{}", |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
16 |
"\\#", |
1826 | 17 |
"\\$", |
18 |
"\\%", |
|
4170 | 19 |
"\\&", |
1826 | 20 |
"'", |
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
21 |
"(", |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
22 |
")", |
4170 | 23 |
"{*}", |
24 |
"+", |
|
1826 | 25 |
",", |
4170 | 26 |
"-", |
1826 | 27 |
".", |
28 |
"/", |
|
29 |
"0", |
|
30 |
"1", |
|
31 |
"2", |
|
32 |
"3", |
|
33 |
"4", |
|
34 |
"5", |
|
35 |
"6", |
|
36 |
"7", |
|
37 |
"8", |
|
38 |
"9", |
|
39 |
":", |
|
40 |
";", |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
41 |
"<", |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
42 |
"=", |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
43 |
">", |
1826 | 44 |
"?", |
45 |
"@", |
|
46 |
"A", |
|
47 |
"B", |
|
48 |
"C", |
|
49 |
"D", |
|
50 |
"E", |
|
51 |
"F", |
|
52 |
"G", |
|
53 |
"H", |
|
54 |
"I", |
|
55 |
"J", |
|
56 |
"K", |
|
57 |
"L", |
|
58 |
"M", |
|
59 |
"N", |
|
60 |
"O", |
|
61 |
"P", |
|
62 |
"Q", |
|
63 |
"R", |
|
64 |
"S", |
|
65 |
"T", |
|
66 |
"U", |
|
67 |
"V", |
|
68 |
"W", |
|
69 |
"X", |
|
70 |
"Y", |
|
71 |
"Z", |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
72 |
"[", |
4170 | 73 |
"\\ttbackslash{}", |
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
74 |
"]", |
1826 | 75 |
"\\^{}", |
4170 | 76 |
"{\\_\\hspace{.344ex}}", |
1826 | 77 |
"`", |
78 |
"a", |
|
79 |
"b", |
|
80 |
"c", |
|
81 |
"d", |
|
82 |
"e", |
|
83 |
"f", |
|
84 |
"g", |
|
85 |
"h", |
|
86 |
"i", |
|
87 |
"j", |
|
88 |
"k", |
|
89 |
"l", |
|
90 |
"m", |
|
91 |
"n", |
|
92 |
"o", |
|
93 |
"p", |
|
94 |
"q", |
|
95 |
"r", |
|
96 |
"s", |
|
97 |
"t", |
|
98 |
"u", |
|
99 |
"v", |
|
100 |
"w", |
|
101 |
"x", |
|
102 |
"y", |
|
103 |
"z", |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
104 |
"\\{", |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
105 |
"|", |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
106 |
"\\}", |
4170 | 107 |
"\\tttilde{}" |
1826 | 108 |
}; |
109 |
/* END_OF_LOW_TABLE */ |
|
110 |
||
111 |
||
112 |
/* |
|
113 |
* conversion table for Hi-8-bit table |
|
114 |
* |
|
115 |
* the row number + START_HIGH_TABLE -1 is the ascii code !! |
|
116 |
* |
|
117 |
* first column is used if destCode is TO_7bit |
|
118 |
* second column is used if destCode is TO_LaTeX |
|
119 |
*/ |
|
120 |
||
121 |
/* do not edit the lines between BEGIN_OF_HI_TABLE and END_OF_HI_TABLE */ |
|
122 |
/* these lines are automatically generated by gen-isa2latex */ |
|
123 |
||
124 |
/* BEGIN_OF_HI_TABLE */ |
|
125 |
char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2] = { |
|
4826 | 126 |
{" " ,"\\ \\ "}, |
127 |
{"\\Gamma" ,"\\mbox{$\\Gamma$}"}, |
|
128 |
{"\\Delta" ,"\\mbox{$\\Delta$}"}, |
|
129 |
{"\\Theta" ,"\\mbox{$\\Theta$}"}, |
|
130 |
{"LAM " ,"\\mbox{$\\Lambda$}"}, |
|
131 |
{"\\Pi" ,"\\mbox{$\\Pi$}"}, |
|
6026 | 132 |
{"SIGMA" ,"\\mbox{$\\Sigma$}"}, |
4826 | 133 |
{"\\Phi" ,"\\mbox{$\\Phi$}"}, |
134 |
{"\\Psi" ,"\\mbox{$\\Psi$}"}, |
|
135 |
{"\\Omega" ,"\\mbox{$\\Omega$}"}, |
|
136 |
{"'a" ,"\\mbox{$\\alpha$}"}, |
|
137 |
{"'b" ,"\\mbox{$\\beta$}"}, |
|
138 |
{"'c" ,"\\mbox{$\\gamma$}"}, |
|
139 |
{"\\delta" ,"\\mbox{$\\delta$}"}, |
|
140 |
{"@" ,"\\mbox{$\\varepsilon$}"}, |
|
141 |
{"\\zeta" ,"\\mbox{$\\zeta$}"}, |
|
142 |
{"\\eta" ,"\\mbox{$\\eta$}"}, |
|
143 |
{"\\vartheta" ,"\\mbox{$\\vartheta$}"}, |
|
144 |
{"\\kappa" ,"\\mbox{$\\kappa$}"}, |
|
145 |
{"%" ,"\\mbox{$\\lambda$}"}, |
|
146 |
{"\\mu" ,"\\mbox{$\\mu$}"}, |
|
147 |
{"\\nu" ,"\\mbox{$\\nu$}"}, |
|
148 |
{"\\xi" ,"\\mbox{$\\xi$}"}, |
|
149 |
{"\\p" ,"\\mbox{$\\pi$}"}, |
|
150 |
{"'r" ,"\\mbox{$\\rho$}"}, |
|
151 |
{"'s" ,"\\mbox{$\\sigma$}"}, |
|
152 |
{"'t" ,"\\mbox{$\\tau$}"}, |
|
153 |
{"\\varphi" ,"\\mbox{$\\varphi$}"}, |
|
154 |
{"\\chi" ,"\\mbox{$\\chi$}"}, |
|
155 |
{"\\psi" ,"\\mbox{$\\psi$}"}, |
|
156 |
{"\\omega" ,"\\mbox{$\\omega$}"}, |
|
5436 | 157 |
{"~ " ,"\\mbox{$\\hspace{-.33ex}\\neg$}"}, |
4826 | 158 |
{"& " ,"\\mbox{$\\hspace{-.185ex}\\wedge\\hspace{-.185ex}$}\\ "}, |
159 |
{"| " ,"\\mbox{$\\hspace{-.185ex}\\vee\\hspace{-.185ex}$}\\ "}, |
|
160 |
{"!" ,"\\mbox{$\\hspace{-.07ex}\\forall$}"}, |
|
161 |
{"? " ,"\\mbox{$\\hspace{-.07ex}\\exists$}"}, |
|
162 |
{"!!" ,"\\mbox{$\\bigwedge$}"}, |
|
163 |
{"\\lceil" ,"\\mbox{$\\lceil$}"}, |
|
164 |
{"\\rceil" ,"\\mbox{$\\rceil$}"}, |
|
165 |
{"\\lfloor" ,"\\mbox{$\\lfloor$}"}, |
|
166 |
{"\\rfloor" ,"\\mbox{$\\rfloor$}"}, |
|
167 |
{"|-" ,"\\mbox{$\\hspace{.49ex}\\vdash\\hspace{.49ex}$}"}, |
|
168 |
{"|=" ,"\\mbox{$\\models$}"}, |
|
169 |
{"[|" ,"\\mbox{$[\\![\\hspace{.32ex}$}"}, |
|
170 |
{"|]" ,"\\mbox{$\\hspace{.32ex}]\\!]$}"}, |
|
171 |
{"." ,"\\mbox{$\\hspace{.28ex}\\cdot\\hspace{.28ex}$}"}, |
|
5436 | 172 |
{":" ,"\\mbox{$\\hspace{.445ex}\\in\\hspace{.445ex}$}"}, |
4826 | 173 |
{" <= " ,"\\mbox{$\\subseteq$}"}, |
174 |
{" Int " ,"\\mbox{$\\cap$}"}, |
|
175 |
{" Un " ,"\\mbox{$\\cup$}"}, |
|
176 |
{"INT " ,"\\mbox{$\\bigcap$}"}, |
|
177 |
{"UN " ,"\\mbox{$\\bigcup$}"}, |
|
178 |
{"\\sqcap" ,"\\mbox{$\\hspace{.29ex}\\sqcap\\hspace{.29ex}$}"}, |
|
179 |
{"\\sqcup" ,"\\mbox{$\\hspace{.29ex}\\sqcup\\hspace{.29ex}$}"}, |
|
180 |
{"glb " ,"\\mbox{$\\overline{|\\,\\,|}$}"}, |
|
181 |
{"LUB " ,"\\mbox{$\\bigsqcup$}"}, |
|
5436 | 182 |
{"UU" ,"\\mbox{$\\hspace{-.29ex}\\bot\\hspace{-.29ex}$}"}, |
4826 | 183 |
{".=" ,"\\mbox{$\\doteq$}"}, |
184 |
{"==" ,"\\mbox{$\\hspace{.29ex}\\equiv\\hspace{.29ex}$}"}, |
|
5436 | 185 |
{"~=" ,"\\mbox{$\\hspace{-.34ex}\\not\\hspace{-.3ex}\\mbox{=}$}"}, |
4826 | 186 |
{"\\sqsubset" ,"\\mbox{$\\hspace{.29ex}\\sqsubset\\hspace{.29ex}$}"}, |
187 |
{"<<" ,"\\mbox{$\\hspace{.29ex}\\sqsubseteq\\hspace{.29ex}$}"}, |
|
188 |
{"<:" ,"\\mbox{$\\hspace{.29ex}\\prec\\hspace{.29ex}$}\\ "}, |
|
189 |
{"<=:" ,"\\mbox{$\\hspace{.29ex}\\preceq\\hspace{.29ex}$}"}, |
|
190 |
{":>" ,"\\mbox{$\\hspace{.29ex}\\succ\\hspace{.29ex}$}\\ "}, |
|
191 |
{"~~" ,"\\mbox{$\\hspace{.29ex}\\approx\\hspace{.29ex}$}"}, |
|
192 |
{"\\sim " ,"\\mbox{$\\hspace{.29ex}\\sim\\hspace{.29ex}$}\\ "}, |
|
193 |
{"\\simeq" ,"\\mbox{$\\hspace{.29ex}\\simeq\\hspace{.29ex}$}"}, |
|
194 |
{"<=" ,"\\mbox{$\\hspace{.29ex}\\le\\hspace{.29ex}$}"}, |
|
195 |
{"::" ,"\\mbox{$:\\hspace{-.07ex}:$}"}, |
|
196 |
{"<-" ,"\\mbox{$\\leftarrow$}"}, |
|
197 |
{"-" ,"\\mbox{$-$}"}, |
|
198 |
{"->" ,"\\mbox{$\\rightarrow$}"}, |
|
199 |
{"<=" ,"\\mbox{$\\Leftarrow$}"}, |
|
200 |
{"=" ,"\\mbox{$=$}"}, |
|
201 |
{"=>" ,"\\mbox{$\\hspace{.12ex}\\Rightarrow$}"}, |
|
202 |
{"\\frown" ,"\\mbox{$\\frown$}"}, |
|
203 |
{"|->" ,"\\mbox{$\\mapsto$}"}, |
|
204 |
{"~>" ,"\\mbox{$\\hspace{.05ex}\\leadsto$}"}, |
|
205 |
{"\\uparrow" ,"\\mbox{$\\uparrow$}"}, |
|
206 |
{"\\downarrow" ,"\\mbox{$\\downarrow$}"}, |
|
5436 | 207 |
{"~:" ,"\\mbox{$\\hspace{.445ex}\\notin\\hspace{.445ex}$}"}, |
4826 | 208 |
{"*" ,"\\mbox{$\\hspace{-.29ex}\\times\\hspace{-.29ex}$}"}, |
209 |
{"++" ,"\\mbox{$\\hspace{.29ex}\\oplus\\hspace{.29ex}$}"}, |
|
210 |
{"--" ,"\\mbox{$\\hspace{.29ex}\\ominus\\hspace{.29ex}$}"}, |
|
211 |
{"**" ,"\\mbox{$\\hspace{.29ex}\\otimes\\hspace{.29ex}$}"}, |
|
212 |
{"//" ,"\\mbox{$\\hspace{.29ex}\\oslash\\hspace{.29ex}$}"}, |
|
213 |
{"\\subset" ,"\\mbox{$\\subset$}"}, |
|
214 |
{"\\infty" ,"\\mbox{$\\infty$}"}, |
|
215 |
{"\\Box" ,"\\mbox{$\\Box$}"}, |
|
216 |
{"<>" ,"\\mbox{$\\hspace{.29ex}\\Diamond\\hspace{.29ex}$}"}, |
|
217 |
{" o " ,"\\mbox{$\\circ$}"}, |
|
218 |
{"\\bullet" ,"\\mbox{$\\bullet$}"}, |
|
219 |
{"||" ,"\\mbox{$\\parallel$}"}, |
|
220 |
{"\\tick" ,"\\mbox{$\\surd$}"}, |
|
221 |
{"\\filter" ,"\\mbox{\\copyright}"} |
|
1826 | 222 |
}; |
223 |
/* END_OF_HI_TABLE */ |
|
224 |
||
225 |
||
226 |
/* |
|
227 |
* conversion table for long ascii and 8bit sequences scanned by lexer |
|
228 |
* |
|
229 |
* first column is used if destCode is TO_7bit |
|
230 |
* second column is used if destCode is TO_LaTeX |
|
231 |
* |
|
232 |
* Row - 1 is the code (longCode) used by the lexer |
|
233 |
*/ |
|
234 |
||
235 |
/* do not edit the lines between BEGIN_OF_SEQ_TABLE and END_OF_SEQ_TABLE */ |
|
236 |
/* these lines are automatically generated by gen-isa2latex */ |
|
237 |
||
238 |
/* BEGIN_OF_SEQ_TABLE */ |
|
239 |
char *translationTableSeq[SEQ_TABLE][2] = { |
|
4170 | 240 |
{"==>" ,"\\mbox{$\\hspace{-.083ex}\\Longrightarrow$}"}, |
241 |
{"-->" ,"\\mbox{$\\longrightarrow$}"}, |
|
242 |
{"?!" ,"\\mbox{$\\exists_1$}"}, |
|
243 |
{"ALL " ,"\\mbox{$\\forall$}"}, |
|
244 |
{"EX " ,"\\mbox{$\\exists$}"}, |
|
245 |
{"<<|" ,"\\mbox{$\\ll\\!\\mid$}"}, |
|
246 |
{"<|" ,"\\mbox{$<\\!\\mid$}"}, |
|
247 |
{"<==" ,"\\mbox{$\\Longleftarrow$}"}, |
|
248 |
{"<=>" ,"\\mbox{$\\Leftrightarrow$}"}, |
|
249 |
{"<--" ,"\\mbox{$\\longleftarrow$}"}, |
|
250 |
{"<->" ,"\\mbox{$\\leftrightarrow$}"}, |
|
5675 | 251 |
{"and" ,"\\mbox{\\bf and}"}, |
4170 | 252 |
{"arities" ,"\\mbox{\\bf arities}"}, |
253 |
{"axclass" ,"\\mbox{\\bf axclass}"}, |
|
254 |
{"constdefs" ,"\\mbox{\\bf constdefs}"}, |
|
255 |
{"consts" ,"\\mbox{\\bf consts}"}, |
|
256 |
{"datatype" ,"\\mbox{\\bf datatype}"}, |
|
257 |
{"defs" ,"\\mbox{\\bf defs}"}, |
|
258 |
{"domain" ,"\\mbox{\\bf domain}"}, |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
259 |
{"end" ,"\\mbox{\\bf end}"}, |
4170 | 260 |
{"inductive" ,"\\mbox{\\bf inductive}"}, |
261 |
{"instance" ,"\\mbox{\\bf instance}"}, |
|
262 |
{"primrec" ,"\\mbox{\\bf primrec}"}, |
|
263 |
{"recdef" ,"\\mbox{\\bf recdef}"}, |
|
264 |
{"rules" ,"\\mbox{\\bf rules}"}, |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4170
diff
changeset
|
265 |
{"syntax" ,"\\mbox{\\bf syntax}"}, |
4170 | 266 |
{"translations" ,"\\mbox{\\bf translations}"}, |
267 |
{"typedef" ,"\\mbox{\\bf typedef}"}, |
|
268 |
{"types" ,"\\mbox{\\bf types}"} |
|
1826 | 269 |
}; |
270 |
/* END_OF_SEQ_TABLE */ |
|
271 |
||
272 |