lib/scripts/feeder.pl
author wenzelm
Thu May 20 20:20:52 2010 +0200 (2010-05-20)
changeset 37012 106c56e916f8
parent 29145 b1c6f4563df7
child 39580 05daab5782f6
permissions -rw-r--r--
enable shell script editor mode;
     1 #
     2 # Author: Markus Wenzel, TU Muenchen
     3 #
     4 # feeder.pl - feed isabelle session
     5 #
     6 
     7 # args
     8 
     9 ($head, $emitpid, $quit, $tail) = @ARGV;
    10 
    11 
    12 # setup signal handlers
    13 
    14 sub hangup { exit(0); }
    15 $SIG{'HUP'} = "hangup";
    16 $SIG{'INT'} = "IGNORE";
    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) {
    30     while (<STDIN>) {
    31 	print;
    32     }
    33 }
    34 
    35 $tail && (print "$tail", "\n");
    36 
    37 
    38 # wait forever
    39 
    40 close STDOUT;
    41 sleep;