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