bin/isatool
author wenzelm
Mon Jan 13 13:20:32 1997 +0100 (1997-01-13)
changeset 2505 50abca9d4043
parent 2434 d3d42a2e7da2
child 2703 5ce1310560ff
permissions -rwxr-xr-x
added -? option;
wenzelm@2344
     1
#!/bin/bash -norc
wenzelm@2293
     2
#
wenzelm@2307
     3
# $Id$
wenzelm@2307
     4
#
wenzelm@2293
     5
# Isabelle tool starter -- keeps your PATH name space clean.
wenzelm@2293
     6
wenzelm@2293
     7
wenzelm@2293
     8
## settings
wenzelm@2293
     9
wenzelm@2293
    10
ISABELLE_HOME=$(dirname $(dirname $0))
wenzelm@2395
    11
. $ISABELLE_HOME/lib/scripts/getsettings || exit 2
wenzelm@2293
    12
wenzelm@2293
    13
wenzelm@2293
    14
## diagnostics
wenzelm@2293
    15
wenzelm@2293
    16
PRG=$(basename $0)
wenzelm@2293
    17
wenzelm@2293
    18
function usage()
wenzelm@2293
    19
{
wenzelm@2293
    20
  echo
wenzelm@2293
    21
  echo "Usage: $PRG TOOL [ARGS ...]"
wenzelm@2293
    22
  echo
wenzelm@2434
    23
  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
wenzelm@2434
    24
  echo "  for specific help."
wenzelm@2293
    25
  echo
wenzelm@2293
    26
  echo "  Availabe tools are:"
wenzelm@2434
    27
  echo
wenzelm@2293
    28
  (
wenzelm@2293
    29
    cd "$ISABELLE_HOME/lib/Tools"
wenzelm@2293
    30
    for T in *
wenzelm@2293
    31
    do
wenzelm@2293
    32
      if [ -f "$T" -a -x "$T" ]; then
wenzelm@2293
    33
        DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
wenzelm@2293
    34
        echo "    $T - $DESCRLINE"
wenzelm@2293
    35
      fi
wenzelm@2293
    36
    done
wenzelm@2293
    37
  )
wenzelm@2293
    38
  echo
wenzelm@2293
    39
  exit 1
wenzelm@2293
    40
}
wenzelm@2293
    41
wenzelm@2293
    42
function fail()
wenzelm@2293
    43
{
wenzelm@2344
    44
  echo "$1" >&2
wenzelm@2293
    45
  exit 2
wenzelm@2293
    46
}
wenzelm@2293
    47
wenzelm@2293
    48
wenzelm@2293
    49
## main
wenzelm@2293
    50
wenzelm@2505
    51
[ $# -lt 1 -o "$1" = "-?" ] && usage
wenzelm@2293
    52
wenzelm@2293
    53
TOOL_BASE="$1"
wenzelm@2293
    54
TOOL="$ISABELLE_HOME/lib/Tools/$1"
wenzelm@2293
    55
shift
wenzelm@2293
    56
wenzelm@2293
    57
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
wenzelm@2293
    58
wenzelm@2293
    59
fail "Tool not found: $TOOL_BASE"