lib/Tools/tty

killed most "no_atp", to make Sledgehammer more complete

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: run Isabelle process with plain tty interaction

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -l NAME      logic image name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
  echo "    -m MODE      add print mode for output"
  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
  echo "    -p NAME      line editor program name"
  echo "                 (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
  echo
  echo "  Run Isabelle process with plain tty interaction and line editor."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

declare -a ISABELLE_OPTIONS=("-I")

LOGIC=""
LINE_EDITOR="$ISABELLE_LINE_EDITOR"

while getopts "l:m:p:o:" OPT
do
  case "$OPT" in
    l)
      LOGIC="$OPTARG"
      ;;
    m)
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
      ;;
    o)
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
      ;;
    p)
      LINE_EDITOR="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }


## main

if [ -n "$LINE_EDITOR" ]; then
  exec "$LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
else
  exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
fi