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