diff -r db49bac6256a -r 5f629ee2502b lib/scripts/feeder
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/feeder	Mon Dec 29 21:39:22 1997 +0100
@@ -0,0 +1,87 @@
+#!/bin/bash
+#
+# $Id$
+#
+# feeder - feed isabelle session
+
+
+## diagnostics
+
+PRG=$(basename $0)
+DIR=$(dirname $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS]"
+  echo
+  echo "  Options are:"
+  echo "    -h TEXT      head text"
+  echo "    -i           ignore INT signal"
+  echo "    -p           emit my pid"
+  echo "    -q           do not pipe stdin"
+  echo "    -s           filter symbols"
+  echo "    -t TEXT      tail text"
+  echo
+  echo "  Output texts (pid, head, stdin, tail), then wait to be terminated."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+HEAD=""
+NOINT=""
+EMITPID=""
+QUIT=""
+SYMBOLS=""
+TAIL=""
+
+while getopts "h:ipqst:" OPT
+do
+  case "$OPT" in
+    h)
+      HEAD="$OPTARG"
+      ;;
+    i)
+      NOINT=true
+      ;;
+    p)
+      EMITPID=true
+      ;;
+    q)
+      QUIT=true
+      ;;
+    s)
+      SYMBOLS=true
+      ;;
+    t)
+      TAIL="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
+
+
+
+## main
+
+exec perl -w $DIR/feeder.pl "$HEAD" "$NOINT" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"