bin/isatool
author wenzelm
Mon Dec 09 16:38:28 1996 +0100 (1996-12-09)
changeset 2344 c3e1eaea4418
parent 2307 508d2a233dbc
child 2395 c24a79fe3651
permissions -rwxr-xr-x
added -norc option;
error output to stderr;
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@2293
    11
. $ISABELLE_HOME/lib/scripts/getsettings
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@2293
    23
  echo "  Start Isabelle utility program TOOL with ARGS."
wenzelm@2293
    24
  echo
wenzelm@2293
    25
  echo "  Availabe tools are:"
wenzelm@2293
    26
  (
wenzelm@2293
    27
    cd "$ISABELLE_HOME/lib/Tools"
wenzelm@2293
    28
    for T in *
wenzelm@2293
    29
    do
wenzelm@2293
    30
      if [ -f "$T" -a -x "$T" ]; then
wenzelm@2293
    31
        DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
wenzelm@2293
    32
        echo "    $T - $DESCRLINE"
wenzelm@2293
    33
      fi
wenzelm@2293
    34
    done
wenzelm@2293
    35
  )
wenzelm@2293
    36
  echo
wenzelm@2293
    37
  exit 1
wenzelm@2293
    38
}
wenzelm@2293
    39
wenzelm@2293
    40
function fail()
wenzelm@2293
    41
{
wenzelm@2344
    42
  echo "$1" >&2
wenzelm@2293
    43
  exit 2
wenzelm@2293
    44
}
wenzelm@2293
    45
wenzelm@2293
    46
wenzelm@2293
    47
## main
wenzelm@2293
    48
wenzelm@2293
    49
[ $# -lt 1 ] && usage
wenzelm@2293
    50
wenzelm@2293
    51
TOOL_BASE="$1"
wenzelm@2293
    52
TOOL="$ISABELLE_HOME/lib/Tools/$1"
wenzelm@2293
    53
shift
wenzelm@2293
    54
wenzelm@2293
    55
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
wenzelm@2293
    56
wenzelm@2293
    57
fail "Tool not found: $TOOL_BASE"