lib/Tools/tty

excursion: commit_exit internally -- checkpoints are fully persistent now;
excursion: do not force intermediate result states yet -- great performance improvement;

#!/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 "    -p NAME      line editor program name"
  echo "                 (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
  echo
  echo "  Run Isabelle process with plain tty interaction, and optional line editor."
  echo
  exit 1
}

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


## process command line

# options

ISABELLE_OPTIONS="-I"
LOGIC=""
LINE_EDITOR="$ISABELLE_LINE_EDITOR"

while getopts "l:m:p:" OPT
do
  case "$OPT" in
    l)
      LOGIC="$OPTARG"
      ;;
    m)
      ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $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