author | wenzelm |
Tue, 10 Dec 1996 12:17:11 +0100 | |
changeset 2358 | 2106d61252b6 |
child 2391 | de76cee7a30c |
permissions | -rw-r--r-- |
2358
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
1 |
# |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
2 |
# $Id$ |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
3 |
# |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
4 |
# symbol_input.pl - translate symbols into \<...> sequences. |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
5 |
# |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
6 |
|
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
7 |
$SIG{INT} = "IGNORE"; |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
8 |
$| = 1; |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
9 |
|
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
10 |
%tab = ( |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
11 |
"\xa1", "\\\\<Gamma>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
12 |
"\xa2", "\\\\<Delta>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
13 |
"\xa3", "\\\\<Theta>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
14 |
"\xa4", "\\\\<Lambda>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
15 |
"\xa5", "\\\\<Pi>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
16 |
"\xa6", "\\\\<Sigma>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
17 |
"\xa7", "\\\\<Phi>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
18 |
"\xa8", "\\\\<Psi>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
19 |
"\xa9", "\\\\<Omega>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
20 |
"\xaa", "\\\\<alpha>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
21 |
"\xab", "\\\\<beta>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
22 |
"\xac", "\\\\<gamma>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
23 |
"\xad", "\\\\<delta>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
24 |
"\xae", "\\\\<epsilon>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
25 |
"\xaf", "\\\\<zeta>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
26 |
"\xb0", "\\\\<eta>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
27 |
"\xb1", "\\\\<theta>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
28 |
"\xb2", "\\\\<kappa>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
29 |
"\xb3", "\\\\<lambda>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
30 |
"\xb4", "\\\\<mu>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
31 |
"\xb5", "\\\\<nu>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
32 |
"\xb6", "\\\\<xi>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
33 |
"\xb7", "\\\\<pi>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
34 |
"\xb8", "\\\\<rho>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
35 |
"\xb9", "\\\\<sigma>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
36 |
"\xba", "\\\\<tau>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
37 |
"\xbb", "\\\\<phi>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
38 |
"\xbc", "\\\\<chi>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
39 |
"\xbd", "\\\\<psi>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
40 |
"\xbe", "\\\\<omega>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
41 |
"\xbf", "\\\\<not>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
42 |
"\xc0", "\\\\<and>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
43 |
"\xc1", "\\\\<or>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
44 |
"\xc2", "\\\\<forall>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
45 |
"\xc3", "\\\\<exists>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
46 |
"\xc4", "\\\\<And>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
47 |
"\xc5", "\\\\<lceil>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
48 |
"\xc6", "\\\\<rceil>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
49 |
"\xc7", "\\\\<lfloor>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
50 |
"\xc8", "\\\\<rfloor>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
51 |
"\xc9", "\\\\<lparr>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
52 |
"\xca", "\\\\<rparr>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
53 |
"\xcb", "\\\\<lbrakk>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
54 |
"\xcc", "\\\\<rbrakk>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
55 |
"\xcd", "\\\\<empty>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
56 |
"\xce", "\\\\<in>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
57 |
"\xcf", "\\\\<subseteq>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
58 |
"\xd0", "\\\\<inter>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
59 |
"\xd1", "\\\\<union>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
60 |
"\xd2", "\\\\<Inter>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
61 |
"\xd3", "\\\\<Union>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
62 |
"\xd4", "\\\\<sqinter>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
63 |
"\xd5", "\\\\<squnion>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
64 |
"\xd6", "\\\\<Sqinter>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
65 |
"\xd7", "\\\\<Squnion>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
66 |
"\xd8", "\\\\<bottom>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
67 |
"\xd9", "\\\\<doteq>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
68 |
"\xda", "\\\\<equiv>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
69 |
"\xdb", "\\\\<noteq>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
70 |
"\xdc", "\\\\<sqsubset>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
71 |
"\xdd", "\\\\<sqsubseteq>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
72 |
"\xde", "\\\\<prec>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
73 |
"\xdf", "\\\\<preceq>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
74 |
"\xe0", "\\\\<succ>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
75 |
"\xe1", "\\\\<succeq>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
76 |
"\xe2", "\\\\<sim>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
77 |
"\xe3", "\\\\<simeq>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
78 |
"\xe4", "\\\\<le>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
79 |
"\xe5", "\\\\<ge>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
80 |
"\xe6", "\\\\<leftarrow>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
81 |
"\xe7", "\\\\<midarrow>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
82 |
"\xe8", "\\\\<rightarrow>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
83 |
"\xe9", "\\\\<Leftarrow>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
84 |
"\xea", "\\\\<Midarrow>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
85 |
"\xeb", "\\\\<Rightarrow>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
86 |
"\xec", "\\\\<rrightarrow>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
87 |
"\xed", "\\\\<mapsto>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
88 |
"\xee", "\\\\<leadsto>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
89 |
"\xef", "\\\\<up>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
90 |
"\xf0", "\\\\<down>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
91 |
"\xf1", "\\\\<notin>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
92 |
"\xf2", "\\\\<times>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
93 |
"\xf3", "\\\\<oplus>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
94 |
"\xf4", "\\\\<ominus>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
95 |
"\xf5", "\\\\<otimes>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
96 |
"\xf6", "\\\\<oslash>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
97 |
"\xf7", "\\\\<natural>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
98 |
"\xf8", "\\\\<infinity>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
99 |
"\xf9", "\\\\<box>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
100 |
"\xfa", "\\\\<diamond>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
101 |
"\xfb", "\\\\<circ>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
102 |
"\xfc", "\\\\<bullet>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
103 |
"\xfd", "\\\\<parallel>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
104 |
"\xfe", "\\\\<tick>", |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
105 |
"\xff", "\\\\<copyright>"); |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
106 |
|
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
107 |
while (<ARGV>) { |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
108 |
s/([\xa1-\xff])/$tab{$1}/g; |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
109 |
print; |
2106d61252b6
symbol_input.pl - translate symbols into \<...> sequences.
wenzelm
parents:
diff
changeset
|
110 |
} |