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
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@4501
    22
wenzelm@4501
    23
$emitpid && (print $$, "\n");
wenzelm@4501
    24
wenzelm@40335
    25
if ($head) {
wenzelm@41616
    26
  utf8::upgrade($head);
wenzelm@40335
    27
  $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
wenzelm@40335
    28
  print $head, "\n";
wenzelm@40335
    29
}
wenzelm@4501
    30
wenzelm@4501
    31
if (!$quit) {
wenzelm@39580
    32
  while (<STDIN>) {
wenzelm@39580
    33
    print;
wenzelm@39580
    34
  }
wenzelm@4501
    35
}
wenzelm@4501
    36
wenzelm@4501
    37
$tail && (print "$tail", "\n");
wenzelm@4501
    38
wenzelm@4501
    39
wenzelm@4504
    40
# wait forever
wenzelm@4501
    41
wenzelm@4501
    42
close STDOUT;
wenzelm@4501
    43
sleep;