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;
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
$SIG{'INT'} = "IGNORE";
wenzelm@4501
    15
wenzelm@4501
    16
wenzelm@4501
    17
# main
wenzelm@4501
    18
wenzelm@4501
    19
#buffer lines
wenzelm@4501
    20
$| = 1;
wenzelm@4501
    21
wenzelm@61187
    22
sub emit {
wenzelm@61187
    23
  my ($text) = @_;
wenzelm@61187
    24
  if ($text) {
wenzelm@61187
    25
    utf8::upgrade($text);
wenzelm@61187
    26
    $text =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
wenzelm@61187
    27
    print $text, "\n";
wenzelm@61187
    28
  }
wenzelm@61187
    29
}
wenzelm@4501
    30
wenzelm@4501
    31
$emitpid && (print $$, "\n");
wenzelm@4501
    32
wenzelm@61187
    33
emit("$head");
wenzelm@4501
    34
wenzelm@4501
    35
if (!$quit) {
wenzelm@39580
    36
  while (<STDIN>) {
wenzelm@39580
    37
    print;
wenzelm@39580
    38
  }
wenzelm@4501
    39
}
wenzelm@4501
    40
wenzelm@61187
    41
emit("$tail");
wenzelm@4501
    42
wenzelm@4501
    43
wenzelm@4504
    44
# wait forever
wenzelm@4501
    45
wenzelm@4501
    46
close STDOUT;
wenzelm@4501
    47
sleep;