lib/scripts/feeder.pl
author haftmann
Sat, 19 Dec 2015 17:03:17 +0100
changeset 61891 76189756ff65
parent 61187 ff00ad5dc03a
permissions -rw-r--r--
documentation on last state of the art concerning interpretation

#
# 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;

sub emit {
  my ($text) = @_;
  if ($text) {
    utf8::upgrade($text);
    $text =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
    print $text, "\n";
  }
}

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

emit("$head");

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

emit("$tail");


# wait forever

close STDOUT;
sleep;