lib/scripts/feeder.pl
author paulson
Mon, 16 Nov 1998 10:36:30 +0100
changeset 5865 2303f5a3036d
parent 4504 2f39aa4bebf3
child 6281 25d41c118304
permissions -rw-r--r--
moved some facts about Pi from ex/PiSets to Fun.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     1
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     2
# $Id$
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     3
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     4
# feeder.pl - feed isabelle session
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     5
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     6
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     7
# args
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     8
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
     9
($head, $emitpid, $quit, $symbols, $tail) = @ARGV;
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    10
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    11
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    12
# symbols translation table
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    13
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    14
%tab = (
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    15
#GENERATED TEXT FOLLOWS - Do not edit!
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    16
  "\xa0", "\\<space2>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    17
  "\xa1", "\\<Gamma>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    18
  "\xa2", "\\<Delta>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    19
  "\xa3", "\\<Theta>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    20
  "\xa4", "\\<Lambda>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    21
  "\xa5", "\\<Pi>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    22
  "\xa6", "\\<Sigma>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    23
  "\xa7", "\\<Phi>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    24
  "\xa8", "\\<Psi>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    25
  "\xa9", "\\<Omega>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    26
  "\xaa", "\\<alpha>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    27
  "\xab", "\\<beta>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    28
  "\xac", "\\<gamma>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    29
  "\xad", "\\<delta>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    30
  "\xae", "\\<epsilon>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    31
  "\xaf", "\\<zeta>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    32
  "\xb0", "\\<eta>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    33
  "\xb1", "\\<theta>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    34
  "\xb2", "\\<kappa>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    35
  "\xb3", "\\<lambda>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    36
  "\xb4", "\\<mu>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    37
  "\xb5", "\\<nu>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    38
  "\xb6", "\\<xi>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    39
  "\xb7", "\\<pi>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    40
  "\xb8", "\\<rho>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    41
  "\xb9", "\\<sigma>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    42
  "\xba", "\\<tau>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    43
  "\xbb", "\\<phi>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    44
  "\xbc", "\\<chi>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    45
  "\xbd", "\\<psi>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    46
  "\xbe", "\\<omega>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    47
  "\xbf", "\\<not>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    48
  "\xc0", "\\<and>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    49
  "\xc1", "\\<or>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    50
  "\xc2", "\\<forall>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    51
  "\xc3", "\\<exists>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    52
  "\xc4", "\\<And>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    53
  "\xc5", "\\<lceil>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    54
  "\xc6", "\\<rceil>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    55
  "\xc7", "\\<lfloor>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    56
  "\xc8", "\\<rfloor>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    57
  "\xc9", "\\<turnstile>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    58
  "\xca", "\\<Turnstile>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    59
  "\xcb", "\\<lbrakk>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    60
  "\xcc", "\\<rbrakk>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    61
  "\xcd", "\\<cdot>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    62
  "\xce", "\\<in>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    63
  "\xcf", "\\<subseteq>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    64
  "\xd0", "\\<inter>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    65
  "\xd1", "\\<union>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    66
  "\xd2", "\\<Inter>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    67
  "\xd3", "\\<Union>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    68
  "\xd4", "\\<sqinter>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    69
  "\xd5", "\\<squnion>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    70
  "\xd6", "\\<Sqinter>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    71
  "\xd7", "\\<Squnion>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    72
  "\xd8", "\\<bottom>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    73
  "\xd9", "\\<doteq>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    74
  "\xda", "\\<equiv>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    75
  "\xdb", "\\<noteq>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    76
  "\xdc", "\\<sqsubset>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    77
  "\xdd", "\\<sqsubseteq>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    78
  "\xde", "\\<prec>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    79
  "\xdf", "\\<preceq>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    80
  "\xe0", "\\<succ>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    81
  "\xe1", "\\<approx>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    82
  "\xe2", "\\<sim>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    83
  "\xe3", "\\<simeq>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    84
  "\xe4", "\\<le>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    85
  "\xe5", "\\<Colon>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    86
  "\xe6", "\\<leftarrow>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    87
  "\xe7", "\\<midarrow>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    88
  "\xe8", "\\<rightarrow>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    89
  "\xe9", "\\<Leftarrow>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    90
  "\xea", "\\<Midarrow>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    91
  "\xeb", "\\<Rightarrow>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    92
  "\xec", "\\<bow>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    93
  "\xed", "\\<mapsto>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    94
  "\xee", "\\<leadsto>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    95
  "\xef", "\\<up>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    96
  "\xf0", "\\<down>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    97
  "\xf1", "\\<notin>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    98
  "\xf2", "\\<times>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    99
  "\xf3", "\\<oplus>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   100
  "\xf4", "\\<ominus>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   101
  "\xf5", "\\<otimes>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   102
  "\xf6", "\\<oslash>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   103
  "\xf7", "\\<subset>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   104
  "\xf8", "\\<infinity>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   105
  "\xf9", "\\<box>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   106
  "\xfa", "\\<diamond>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   107
  "\xfb", "\\<circ>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   108
  "\xfc", "\\<bullet>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   109
  "\xfd", "\\<parallel>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   110
  "\xfe", "\\<surd>",
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   111
  "\xff", "\\<copyright>"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   112
#END OF GENERATED TEXT
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   113
);
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   114
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   115
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
   116
# setup signal handlers
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   117
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
   118
sub hangup { exit(0); }
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   119
$SIG{'HUP'} = "hangup";
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
   120
$SIG{'INT'} = "IGNORE";
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   121
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   122
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   123
# main
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   124
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   125
#buffer lines
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   126
$| = 1;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   127
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   128
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   129
$emitpid && (print $$, "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   130
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   131
$head && (print "$head", "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   132
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   133
if (!$quit) {
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   134
    while (<STDIN>) {
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   135
	$symbols && (s/([\xa1-\xff])/\\$tab{$1}/g);
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   136
	print;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   137
    }
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   138
}
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   139
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   140
$tail && (print "$tail", "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   141
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   142
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
   143
# wait forever
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   144
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   145
close STDOUT;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
   146
sleep;