--- a/lib/scripts/feeder.pl Wed Mar 09 16:53:14 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# feeder.pl - feed isabelle session
-#
-
-# args
-
-($head, $emitpid, $quit, $tail) = @ARGV;
-
-
-# setup signal handlers
-
-$SIG{'INT'} = "IGNORE";
-
-
-# main
-
-#buffer lines
-$| = 1;
-
-sub emit {
- my ($text) = @_;
- if ($text) {
- utf8::upgrade($text);
- $text =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
- print $text, "\n";
- }
-}
-
-$emitpid && (print $$, "\n");
-
-emit("$head");
-
-if (!$quit) {
- while (<STDIN>) {
- print;
- }
-}
-
-emit("$tail");
-
-
-# wait forever
-
-close STDOUT;
-sleep;