| author | blanchet | 
| Wed, 23 May 2012 21:19:48 +0200 | |
| changeset 47973 | 9af7e5caf16f | 
| parent 47868 | 32c03d45fffe | 
| child 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 | ||
| 22 | ||
| 23 | $emitpid && (print $$, "\n"); | |
| 24 | ||
| 40335 
3e4bb6e7c3ca
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
 wenzelm parents: 
39580diff
changeset | 25 | if ($head) {
 | 
| 41616 
aa002926cbf1
potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
 wenzelm parents: 
40335diff
changeset | 26 | utf8::upgrade($head); | 
| 40335 
3e4bb6e7c3ca
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
 wenzelm parents: 
39580diff
changeset | 27 |   $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
 | 
| 
3e4bb6e7c3ca
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
 wenzelm parents: 
39580diff
changeset | 28 | print $head, "\n"; | 
| 
3e4bb6e7c3ca
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
 wenzelm parents: 
39580diff
changeset | 29 | } | 
| 4501 | 30 | |
| 31 | if (!$quit) {
 | |
| 39580 | 32 |   while (<STDIN>) {
 | 
| 33 | print; | |
| 34 | } | |
| 4501 | 35 | } | 
| 36 | ||
| 37 | $tail && (print "$tail", "\n"); | |
| 38 | ||
| 39 | ||
| 4504 | 40 | # wait forever | 
| 4501 | 41 | |
| 42 | close STDOUT; | |
| 43 | sleep; |