diff -r acd17a6ce17d -r 27f90319a499 lib/scripts/feeder.pl
--- 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;