lib/scripts/feeder.pl
author blanchet
Tue, 05 Nov 2013 05:48:08 +0100
changeset 54254 d1478807f287
parent 47868 32c03d45fffe
child 61187 ff00ad5dc03a
permissions -rw-r--r--
generalize types when synthetizing n2m (co)recursors, to facilitate reuse

#
# Author: Markus Wenzel, TU Muenchen
#
# feeder.pl - feed isabelle session
#

# args

($head, $emitpid, $quit, $tail) = @ARGV;


# setup signal handlers

$SIG{'INT'} = "IGNORE";


# main

#buffer lines
$| = 1;


$emitpid && (print $$, "\n");

if ($head) {
  utf8::upgrade($head);
  $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
  print $head, "\n";
}

if (!$quit) {
  while (<STDIN>) {
    print;
  }
}

$tail && (print "$tail", "\n");


# wait forever

close STDOUT;
sleep;