--- /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"