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