author | wenzelm |
Wed, 10 Feb 2016 14:14:43 +0100 | |
changeset 62278 | c04e97be39d3 |
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; |