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