lib/scripts/feeder.pl
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 61187 ff00ad5dc03a
permissions -rw-r--r--
updated for release;
     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 $SIG{'INT'} = "IGNORE";
    15 
    16 
    17 # main
    18 
    19 #buffer lines
    20 $| = 1;
    21 
    22 sub emit {
    23   my ($text) = @_;
    24   if ($text) {
    25     utf8::upgrade($text);
    26     $text =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
    27     print $text, "\n";
    28   }
    29 }
    30 
    31 $emitpid && (print $$, "\n");
    32 
    33 emit("$head");
    34 
    35 if (!$quit) {
    36   while (<STDIN>) {
    37     print;
    38   }
    39 }
    40 
    41 emit("$tail");
    42 
    43 
    44 # wait forever
    45 
    46 close STDOUT;
    47 sleep;