bin/isatool
author wenzelm
Mon Dec 02 18:14:32 1996 +0100 (1996-12-02)
changeset 2293 749757db3ead
child 2307 508d2a233dbc
permissions -rwxr-xr-x
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm@2293
     1
#!/bin/bash
wenzelm@2293
     2
#
wenzelm@2293
     3
# Isabelle tool starter -- keeps your PATH name space clean.
wenzelm@2293
     4
#
wenzelm@2293
     5
# $Id$
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
wenzelm@2293
    15
## diagnostics
wenzelm@2293
    16
wenzelm@2293
    17
PRG=$(basename $0)
wenzelm@2293
    18
wenzelm@2293
    19
function usage()
wenzelm@2293
    20
{
wenzelm@2293
    21
  echo
wenzelm@2293
    22
  echo "Usage: $PRG TOOL [ARGS ...]"
wenzelm@2293
    23
  echo
wenzelm@2293
    24
  echo "  Start Isabelle utility program TOOL with ARGS."
wenzelm@2293
    25
  echo
wenzelm@2293
    26
  echo "  Availabe tools are:"
wenzelm@2293
    27
  (
wenzelm@2293
    28
    cd "$ISABELLE_HOME/lib/Tools"
wenzelm@2293
    29
    for T in *
wenzelm@2293
    30
    do
wenzelm@2293
    31
      if [ -f "$T" -a -x "$T" ]; then
wenzelm@2293
    32
        DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
wenzelm@2293
    33
        echo "    $T - $DESCRLINE"
wenzelm@2293
    34
      fi
wenzelm@2293
    35
    done
wenzelm@2293
    36
  )
wenzelm@2293
    37
  echo
wenzelm@2293
    38
  exit 1
wenzelm@2293
    39
}
wenzelm@2293
    40
wenzelm@2293
    41
function fail()
wenzelm@2293
    42
{
wenzelm@2293
    43
  echo "$1"
wenzelm@2293
    44
  exit 2
wenzelm@2293
    45
}
wenzelm@2293
    46
wenzelm@2293
    47
wenzelm@2293
    48
wenzelm@2293
    49
## main
wenzelm@2293
    50
wenzelm@2293
    51
[ $# -lt 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"