bin/isatool
author wenzelm
Fri Mar 08 16:24:06 2002 +0100 (2002-03-08)
changeset 13049 ce180e5b7fa0
parent 11044 5873a05b4d21
child 14981 e73f8140af78
permissions -rwxr-xr-x
tuned;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # Isabelle tool starter -- provides settings environment
     8 # and keeps your PATH name space clean.
     9 
    10 
    11 ## settings
    12 
    13 PRG="$(basename "$0")"
    14 
    15 ISABELLE_HOME="$(dirname "$0")/.."
    16 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    17   { echo "$PRG probably not called from its original place!"; exit 2; }
    18 
    19 
    20 ## diagnostics
    21 
    22 function usage()
    23 {
    24   echo
    25   echo "Usage: $PRG TOOL [ARGS ...]"
    26   echo
    27   echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
    28   echo "  for more specific help."
    29   echo
    30   echo "  Available tools are:"
    31   (
    32     ORIG_IFS="$IFS"
    33     IFS=":"
    34     for DIR in $ISABELLE_TOOLS
    35     do
    36       cd "$DIR"
    37       echo
    38       for T in *
    39       do
    40         if [ -f "$T" -a -x "$T" ]; then
    41           DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
    42           echo "    $T - $DESCRLINE"
    43         fi
    44       done
    45     done
    46     IFS="$ORIG_IFS"
    47   )
    48   echo
    49   exit 1
    50 }
    51 
    52 function fail()
    53 {
    54   echo "$1" >&2
    55   exit 2
    56 }
    57 
    58 
    59 ## args
    60 
    61 [ "$#" -lt 1 -o "$1" = "-?" ] && usage
    62 
    63 TOOLNAME="$1"
    64 shift
    65 
    66 
    67 ## main
    68 
    69 ORIG_IFS="$IFS"
    70 IFS=":"
    71 for DIR in $ISABELLE_TOOLS
    72 do
    73   TOOL="$DIR/$TOOLNAME"
    74   [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
    75 done
    76 IFS="$ORIG_IFS"
    77 
    78 fail "Unknown Isabelle tool: $TOOLNAME"