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