lib/Tools/tty
author wenzelm
Thu Apr 24 00:29:55 2014 +0200 (2014-04-24)
changeset 56686 2386d1a3ca8f
parent 52062 4f91262e7f33
permissions -rwxr-xr-x
canonical list operations, as in ML;
avoid odd mutable data structures;
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@52062
    17
  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
wenzelm@25632
    18
  echo "    -p NAME      line editor program name"
wenzelm@25633
    19
  echo "                 (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
wenzelm@25632
    20
  echo
wenzelm@48572
    21
  echo "  Run Isabelle process with plain tty interaction and line editor."
wenzelm@25632
    22
  echo
wenzelm@25632
    23
  exit 1
wenzelm@25632
    24
}
wenzelm@25632
    25
wenzelm@25632
    26
function fail()
wenzelm@25632
    27
{
wenzelm@25632
    28
  echo "$1" >&2
wenzelm@25632
    29
  exit 2
wenzelm@25632
    30
}
wenzelm@25632
    31
wenzelm@25632
    32
wenzelm@25632
    33
## process command line
wenzelm@25632
    34
wenzelm@25632
    35
# options
wenzelm@25632
    36
wenzelm@52062
    37
declare -a ISABELLE_OPTIONS=("-I")
wenzelm@52062
    38
wenzelm@25632
    39
LOGIC=""
wenzelm@25632
    40
LINE_EDITOR="$ISABELLE_LINE_EDITOR"
wenzelm@25632
    41
wenzelm@52062
    42
while getopts "l:m:p:o:" OPT
wenzelm@25632
    43
do
wenzelm@25632
    44
  case "$OPT" in
wenzelm@25632
    45
    l)
wenzelm@25632
    46
      LOGIC="$OPTARG"
wenzelm@25632
    47
      ;;
wenzelm@25632
    48
    m)
wenzelm@52062
    49
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
wenzelm@52062
    50
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
wenzelm@52062
    51
      ;;
wenzelm@52062
    52
    o)
wenzelm@52062
    53
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
wenzelm@52062
    54
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
wenzelm@25632
    55
      ;;
wenzelm@25632
    56
    p)
wenzelm@25632
    57
      LINE_EDITOR="$OPTARG"
wenzelm@25632
    58
      ;;
wenzelm@25632
    59
    \?)
wenzelm@25632
    60
      usage
wenzelm@25632
    61
      ;;
wenzelm@25632
    62
  esac
wenzelm@25632
    63
done
wenzelm@25632
    64
wenzelm@25632
    65
shift $(($OPTIND - 1))
wenzelm@25632
    66
wenzelm@25632
    67
wenzelm@25632
    68
# args
wenzelm@25632
    69
wenzelm@25632
    70
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
wenzelm@25632
    71
wenzelm@25632
    72
wenzelm@25632
    73
## main
wenzelm@25632
    74
wenzelm@25632
    75
if [ -n "$LINE_EDITOR" ]; then
wenzelm@52062
    76
  exec "$LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
wenzelm@25632
    77
else
wenzelm@52062
    78
  exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
wenzelm@25632
    79
fi