#!/usr/bin/env 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 "    -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

#set by configure

AUTO_PERL=perl

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