| author | noschinl | 
| Fri, 06 Sep 2013 10:56:40 +0200 | |
| changeset 53430 | d92578436d47 | 
| 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: 
39580 
diff
changeset
 | 
25  | 
if ($head) {
 | 
| 
41616
 
aa002926cbf1
potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
 
wenzelm 
parents: 
40335 
diff
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: 
39580 
diff
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: 
39580 
diff
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: 
39580 
diff
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;  |