| author | haftmann |
| Wed, 17 Feb 2016 21:51:57 +0100 | |
| changeset 62348 | 9a5f43dac883 |
| 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:
47868
diff
changeset
|
22 |
sub emit {
|
|
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents:
47868
diff
changeset
|
23 |
my ($text) = @_; |
|
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents:
47868
diff
changeset
|
24 |
if ($text) {
|
|
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents:
47868
diff
changeset
|
25 |
utf8::upgrade($text); |
|
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents:
47868
diff
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:
47868
diff
changeset
|
27 |
print $text, "\n"; |
|
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents:
47868
diff
changeset
|
28 |
} |
|
ff00ad5dc03a
recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents:
47868
diff
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:
47868
diff
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:
47868
diff
changeset
|
41 |
emit("$tail");
|
| 4501 | 42 |
|
43 |
||
| 4504 | 44 |
# wait forever |
| 4501 | 45 |
|
46 |
close STDOUT; |
|
47 |
sleep; |