lib/scripts/feeder
author wenzelm
Fri, 16 Apr 2010 10:52:10 +0200
changeset 36162 0bd034a80a9a
parent 29145 b1c6f4563df7
child 40335 3e4bb6e7c3ca
permissions -rwxr-xr-x
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# 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 "    -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=""
TAIL=""

while getopts "h:pqt:" OPT
do
  case "$OPT" in
    h)
      HEAD="$OPTARG"
      ;;
    p)
      EMITPID=true
      ;;
    q)
      QUIT=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" "$EMITPID" "$QUIT" "$TAIL"