lib/scripts/feeder.pl
author wenzelm
Mon, 01 Aug 2005 19:20:49 +0200
changeset 16996 32afaa947f6e
parent 14981 e73f8140af78
child 29145 b1c6f4563df7
permissions -rw-r--r--
determine Poly/ML runtime system version
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$
9789
wenzelm
parents: 6281
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     4
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     5
# feeder.pl - feed isabelle session
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     6
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     7
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     8
# args
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     9
12111
d942348d8faf got rid of obsolete input filtering;
wenzelm
parents: 9961
diff changeset
    10
($head, $emitpid, $quit, $tail) = @ARGV;
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    11
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    12
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    13
# setup signal handlers
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    14
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    15
sub hangup { exit(0); }
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    16
$SIG{'HUP'} = "hangup";
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    17
$SIG{'INT'} = "IGNORE";
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    18
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    19
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    20
# main
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    21
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    22
#buffer lines
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    23
$| = 1;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    24
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    25
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    26
$emitpid && (print $$, "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    27
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    28
$head && (print "$head", "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    29
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    30
if (!$quit) {
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    31
    while (<STDIN>) {
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    32
	print;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    33
    }
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    34
}
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    35
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    36
$tail && (print "$tail", "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    37
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    38
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    39
# wait forever
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    40
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    41
close STDOUT;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    42
sleep;