lib/Tools/tty
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 29143 72c960b2b83e
child 48572 af0f5560ac94
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
wenzelm@25632
     1
#!/usr/bin/env bash
wenzelm@25632
     2
#
wenzelm@25632
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@25632
     4
#
wenzelm@25632
     5
# DESCRIPTION: run Isabelle process with plain tty interaction
wenzelm@25632
     6
wenzelm@25632
     7
PRG="$(basename "$0")"
wenzelm@25632
     8
wenzelm@25632
     9
function usage()
wenzelm@25632
    10
{
wenzelm@25632
    11
  echo
wenzelm@28650
    12
  echo "Usage: isabelle $PRG [OPTIONS]"
wenzelm@25632
    13
  echo
wenzelm@25632
    14
  echo "  Options are:"
wenzelm@25633
    15
  echo "    -l NAME      logic image name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
wenzelm@25632
    16
  echo "    -m MODE      add print mode for output"
wenzelm@25632
    17
  echo "    -p NAME      line editor program name"
wenzelm@25633
    18
  echo "                 (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
wenzelm@25632
    19
  echo
wenzelm@25632
    20
  echo "  Run Isabelle process with plain tty interaction, and optional line editor."
wenzelm@25632
    21
  echo
wenzelm@25632
    22
  exit 1
wenzelm@25632
    23
}
wenzelm@25632
    24
wenzelm@25632
    25
function fail()
wenzelm@25632
    26
{
wenzelm@25632
    27
  echo "$1" >&2
wenzelm@25632
    28
  exit 2
wenzelm@25632
    29
}
wenzelm@25632
    30
wenzelm@25632
    31
wenzelm@25632
    32
## process command line
wenzelm@25632
    33
wenzelm@25632
    34
# options
wenzelm@25632
    35
wenzelm@25632
    36
ISABELLE_OPTIONS="-I"
wenzelm@25632
    37
LOGIC=""
wenzelm@25632
    38
LINE_EDITOR="$ISABELLE_LINE_EDITOR"
wenzelm@25632
    39
wenzelm@25632
    40
while getopts "l:m:p:" OPT
wenzelm@25632
    41
do
wenzelm@25632
    42
  case "$OPT" in
wenzelm@25632
    43
    l)
wenzelm@25632
    44
      LOGIC="$OPTARG"
wenzelm@25632
    45
      ;;
wenzelm@25632
    46
    m)
wenzelm@25637
    47
      ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
wenzelm@25632
    48
      ;;
wenzelm@25632
    49
    p)
wenzelm@25632
    50
      LINE_EDITOR="$OPTARG"
wenzelm@25632
    51
      ;;
wenzelm@25632
    52
    \?)
wenzelm@25632
    53
      usage
wenzelm@25632
    54
      ;;
wenzelm@25632
    55
  esac
wenzelm@25632
    56
done
wenzelm@25632
    57
wenzelm@25632
    58
shift $(($OPTIND - 1))
wenzelm@25632
    59
wenzelm@25632
    60
wenzelm@25632
    61
# args
wenzelm@25632
    62
wenzelm@25632
    63
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
wenzelm@25632
    64
wenzelm@25632
    65
wenzelm@25632
    66
## main
wenzelm@25632
    67
wenzelm@25632
    68
if [ -n "$LINE_EDITOR" ]; then
wenzelm@28502
    69
  exec "$LINE_EDITOR" "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
wenzelm@25632
    70
else
wenzelm@28502
    71
  exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
wenzelm@25632
    72
fi