| 4501 |      1 | #
 | 
|  |      2 | # $Id$
 | 
| 9789 |      3 | # Author: Markus Wenzel, TU Muenchen
 | 
| 4501 |      4 | #
 | 
|  |      5 | # feeder.pl - feed isabelle session
 | 
|  |      6 | #
 | 
|  |      7 | 
 | 
|  |      8 | # args
 | 
|  |      9 | 
 | 
| 12111 |     10 | ($head, $emitpid, $quit, $tail) = @ARGV;
 | 
| 4501 |     11 | 
 | 
|  |     12 | 
 | 
| 4504 |     13 | # setup signal handlers
 | 
| 4501 |     14 | 
 | 
| 4504 |     15 | sub hangup { exit(0); }
 | 
| 4501 |     16 | $SIG{'HUP'} = "hangup";
 | 
| 4504 |     17 | $SIG{'INT'} = "IGNORE";
 | 
| 4501 |     18 | 
 | 
|  |     19 | 
 | 
|  |     20 | # main
 | 
|  |     21 | 
 | 
|  |     22 | #buffer lines
 | 
|  |     23 | $| = 1;
 | 
|  |     24 | 
 | 
|  |     25 | 
 | 
|  |     26 | $emitpid && (print $$, "\n");
 | 
|  |     27 | 
 | 
|  |     28 | $head && (print "$head", "\n");
 | 
|  |     29 | 
 | 
|  |     30 | if (!$quit) {
 | 
|  |     31 |     while (<STDIN>) {
 | 
|  |     32 | 	print;
 | 
|  |     33 |     }
 | 
|  |     34 | }
 | 
|  |     35 | 
 | 
|  |     36 | $tail && (print "$tail", "\n");
 | 
|  |     37 | 
 | 
|  |     38 | 
 | 
| 4504 |     39 | # wait forever
 | 
| 4501 |     40 | 
 | 
|  |     41 | close STDOUT;
 | 
|  |     42 | sleep;
 |