| author | nipkow | 
| Wed, 11 Nov 2015 16:42:30 +0100 | |
| changeset 61638 | 7ffc9c4f1f74 | 
| parent 61187 | ff00ad5dc03a | 
| permissions | -rw-r--r-- | 
| 4501 | 1 | # | 
| 9789 | 2 | # Author: Markus Wenzel, TU Muenchen | 
| 4501 | 3 | # | 
| 4 | # feeder.pl - feed isabelle session | |
| 5 | # | |
| 6 | ||
| 7 | # args | |
| 8 | ||
| 12111 | 9 | ($head, $emitpid, $quit, $tail) = @ARGV; | 
| 4501 | 10 | |
| 11 | ||
| 4504 | 12 | # setup signal handlers | 
| 4501 | 13 | |
| 4504 | 14 | $SIG{'INT'} = "IGNORE";
 | 
| 4501 | 15 | |
| 16 | ||
| 17 | # main | |
| 18 | ||
| 19 | #buffer lines | |
| 20 | $| = 1; | |
| 21 | ||
| 61187 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 22 | sub emit {
 | 
| 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 23 | my ($text) = @_; | 
| 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 24 |   if ($text) {
 | 
| 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 25 | utf8::upgrade($text); | 
| 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 26 |     $text =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
 | 
| 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 27 | print $text, "\n"; | 
| 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 28 | } | 
| 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 29 | } | 
| 4501 | 30 | |
| 31 | $emitpid && (print $$, "\n"); | |
| 32 | ||
| 61187 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 33 | emit("$head");
 | 
| 4501 | 34 | |
| 35 | if (!$quit) {
 | |
| 39580 | 36 |   while (<STDIN>) {
 | 
| 37 | print; | |
| 38 | } | |
| 4501 | 39 | } | 
| 40 | ||
| 61187 
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
 wenzelm parents: 
47868diff
changeset | 41 | emit("$tail");
 | 
| 4501 | 42 | |
| 43 | ||
| 4504 | 44 | # wait forever | 
| 4501 | 45 | |
| 46 | close STDOUT; | |
| 47 | sleep; |