lib/Tools/tty
author wenzelm
Thu, 15 May 2008 17:37:18 +0200
changeset 26899 29bb3d1de3bc
parent 25637 e50550be4dfa
child 28502 6b0e3e4e1891
permissions -rwxr-xr-x
hyperref is always enabled (also works with xdvi, dvips); replaced darkblue by generic linkcolor; reduced verbosity;
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
# $Id$
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     5
#
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     6
# DESCRIPTION: run Isabelle process with plain tty interaction
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     7
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     8
PRG="$(basename "$0")"
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
     9
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    10
function usage()
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    11
{
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    12
  echo
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    13
  echo "Usage: $PRG [OPTIONS]"
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    14
  echo
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    15
  echo "  Options are:"
25633
a5d8e5c7a65a tuned diagnostics;
wenzelm
parents: 25632
diff changeset
    16
  echo "    -l NAME      logic image name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
25632
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    17
  echo "    -m MODE      add print mode for output"
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    18
  echo "    -p NAME      line editor program name"
25633
a5d8e5c7a65a tuned diagnostics;
wenzelm
parents: 25632
diff changeset
    19
  echo "                 (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
25632
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    20
  echo
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    21
  echo "  Run Isabelle process with plain tty interaction, and optional line editor."
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    22
  echo
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    23
  exit 1
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
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    26
function fail()
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    27
{
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    28
  echo "$1" >&2
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    29
  exit 2
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
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    33
## process command line
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    34
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    35
# options
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    36
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    37
ISABELLE_OPTIONS="-I"
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    38
LOGIC=""
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    39
LINE_EDITOR="$ISABELLE_LINE_EDITOR"
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    40
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    41
while getopts "l:m:p:" OPT
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    42
do
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    43
  case "$OPT" in
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    44
    l)
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    45
      LOGIC="$OPTARG"
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    46
      ;;
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    47
    m)
25637
e50550be4dfa option -m: avoid additional quoting;
wenzelm
parents: 25633
diff changeset
    48
      ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
25632
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    49
      ;;
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    50
    p)
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    51
      LINE_EDITOR="$OPTARG"
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
    \?)
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    54
      usage
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    55
      ;;
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    56
  esac
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    57
done
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    58
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    59
shift $(($OPTIND - 1))
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
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    62
# args
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    63
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    64
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
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
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    67
## main
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    68
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    69
if [ -n "$LINE_EDITOR" ]; then
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    70
  exec "$LINE_EDITOR" "$ISABELLE" $ISABELLE_OPTIONS "$LOGIC"
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    71
else
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    72
  exec "$ISABELLE" $ISABELLE_OPTIONS "$LOGIC"
01a8d27a0857 run Isabelle process with plain tty interaction;
wenzelm
parents:
diff changeset
    73
fi