--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/symbol_input.pl Mon Dec 16 15:45:02 1996 +0100
@@ -0,0 +1,112 @@
+# Title: Distribution/lib/scripts/symbol_input.pl
+# ID: $Id$
+# Author: Markus Wenzel, David von Oheimb
+# Copyright 1996 Technische Universitaet Muenchen
+#
+# translate symbols into \<...> sequences.
+# table must be consistent with Pure/Syntax/symbol_font.ML
+
+%tab = (
+ "\xa1", "\\\\<Gamma>",
+ "\xa2", "\\\\<Delta>",
+ "\xa3", "\\\\<Theta>",
+ "\xa4", "\\\\<Lambda>",
+ "\xa5", "\\\\<Pi>",
+ "\xa6", "\\\\<Sigma>",
+ "\xa7", "\\\\<Phi>",
+ "\xa8", "\\\\<Psi>",
+ "\xa9", "\\\\<Omega>",
+ "\xaa", "\\\\<alpha>",
+ "\xab", "\\\\<beta>",
+ "\xac", "\\\\<gamma>",
+ "\xad", "\\\\<delta>",
+ "\xae", "\\\\<epsilon>",
+ "\xaf", "\\\\<zeta>",
+ "\xb0", "\\\\<eta>",
+ "\xb1", "\\\\<theta>",
+ "\xb2", "\\\\<kappa>",
+ "\xb3", "\\\\<lambda>",
+ "\xb4", "\\\\<mu>",
+ "\xb5", "\\\\<nu>",
+ "\xb6", "\\\\<xi>",
+ "\xb7", "\\\\<pi>",
+ "\xb8", "\\\\<rho>",
+ "\xb9", "\\\\<sigma>",
+ "\xba", "\\\\<tau>",
+ "\xbb", "\\\\<phi>",
+ "\xbc", "\\\\<chi>",
+ "\xbd", "\\\\<psi>",
+ "\xbe", "\\\\<omega>",
+ "\xbf", "\\\\<not>",
+ "\xc0", "\\\\<and>",
+ "\xc1", "\\\\<or>",
+ "\xc2", "\\\\<forall>",
+ "\xc3", "\\\\<exists>",
+ "\xc4", "\\\\<And>",
+ "\xc5", "\\\\<lceil>",
+ "\xc6", "\\\\<rceil>",
+ "\xc7", "\\\\<lfloor>",
+ "\xc8", "\\\\<rfloor>",
+ "\xc9", "\\\\<lparr>",
+ "\xca", "\\\\<rparr>",
+ "\xcb", "\\\\<lbrakk>",
+ "\xcc", "\\\\<rbrakk>",
+ "\xcd", "\\\\<empty>",
+ "\xce", "\\\\<in>",
+ "\xcf", "\\\\<subseteq>",
+ "\xd0", "\\\\<inter>",
+ "\xd1", "\\\\<union>",
+ "\xd2", "\\\\<Inter>",
+ "\xd3", "\\\\<Union>",
+ "\xd4", "\\\\<sqinter>",
+ "\xd5", "\\\\<squnion>",
+ "\xd6", "\\\\<Sqinter>",
+ "\xd7", "\\\\<Squnion>",
+ "\xd8", "\\\\<bottom>",
+ "\xd9", "\\\\<doteq>",
+ "\xda", "\\\\<equiv>",
+ "\xdb", "\\\\<noteq>",
+ "\xdc", "\\\\<sqsubset>",
+ "\xdd", "\\\\<sqsubseteq>",
+ "\xde", "\\\\<prec>",
+ "\xdf", "\\\\<preceq>",
+ "\xe0", "\\\\<succ>",
+ "\xe1", "\\\\<succeq>",
+ "\xe2", "\\\\<sim>",
+ "\xe3", "\\\\<simeq>",
+ "\xe4", "\\\\<le>",
+ "\xe5", "\\\\<ge>",
+ "\xe6", "\\\\<leftarrow>",
+ "\xe7", "\\\\<midarrow>",
+ "\xe8", "\\\\<rightarrow>",
+ "\xe9", "\\\\<Leftarrow>",
+ "\xea", "\\\\<Midarrow>",
+ "\xeb", "\\\\<Rightarrow>",
+ "\xec", "\\\\<rrightarrow>",
+ "\xed", "\\\\<mapsto>",
+ "\xee", "\\\\<leadsto>",
+ "\xef", "\\\\<up>",
+ "\xf0", "\\\\<down>",
+ "\xf1", "\\\\<notin>",
+ "\xf2", "\\\\<times>",
+ "\xf3", "\\\\<oplus>",
+ "\xf4", "\\\\<ominus>",
+ "\xf5", "\\\\<otimes>",
+ "\xf6", "\\\\<oslash>",
+ "\xf7", "\\\\<natural>",
+ "\xf8", "\\\\<infinity>",
+ "\xf9", "\\\\<box>",
+ "\xfa", "\\\\<diamond>",
+ "\xfb", "\\\\<circ>",
+ "\xfc", "\\\\<bullet>",
+ "\xfd", "\\\\<parallel>",
+ "\xfe", "\\\\<tick>",
+ "\xff", "\\\\<copyright>");
+
+$SIG{INT} = "IGNORE";
+$| = 1;
+
+while (<ARGV>) {
+ s/([\xa1-\xff])/$tab{$1}/g;
+ print;
+}