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