lib/scripts/feeder.pl
author nipkow
Fri May 30 18:13:40 2014 +0200 (2014-05-30)
changeset 57136 653e56c6c963
parent 47868 32c03d45fffe
child 61187 ff00ad5dc03a
permissions -rw-r--r--
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
     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 
    23 $emitpid && (print $$, "\n");
    24 
    25 if ($head) {
    26   utf8::upgrade($head);
    27   $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
    28   print $head, "\n";
    29 }
    30 
    31 if (!$quit) {
    32   while (<STDIN>) {
    33     print;
    34   }
    35 }
    36 
    37 $tail && (print "$tail", "\n");
    38 
    39 
    40 # wait forever
    41 
    42 close STDOUT;
    43 sleep;