lib/scripts/feeder

fixed hrefs: index.html;

#!/bin/bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# 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 "    -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=""
EMITPID=""
QUIT=""
SYMBOLS=""
TAIL=""

while getopts "h:pqst:" OPT
do
  case "$OPT" in
    h)
      HEAD="$OPTARG"
      ;;
    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

#set by configure
AUTO_PERL=perl

exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"