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