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