bin/isatool
author wenzelm
Fri Apr 11 17:30:15 1997 +0200 (1997-04-11)
changeset 2936 bd33e7aae062
parent 2787 33931e1023e3
child 3007 e5efa177ee0c
permissions -rwxr-xr-x
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm@2737
     1
#!/bin/bash -norc
wenzelm@2293
     2
#
wenzelm@2307
     3
# $Id$
wenzelm@2307
     4
#
wenzelm@2735
     5
# Isabelle tool starter -- provides settings environment,
wenzelm@2787
     6
#   and keeps your PATH name space clean.
wenzelm@2293
     7
wenzelm@2293
     8
wenzelm@2293
     9
## settings
wenzelm@2293
    10
wenzelm@2703
    11
PRG=$(basename $0)
wenzelm@2703
    12
wenzelm@2735
    13
ISABELLE_HOME=$(dirname $0)/..
wenzelm@2735
    14
. $ISABELLE_HOME/lib/scripts/getsettings || \
wenzelm@2936
    15
  { echo "$PRG probably not called from its original place!"; exit 2; }
wenzelm@2293
    16
wenzelm@2293
    17
wenzelm@2293
    18
## diagnostics
wenzelm@2293
    19
wenzelm@2787
    20
TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ")
wenzelm@2787
    21
wenzelm@2293
    22
function usage()
wenzelm@2293
    23
{
wenzelm@2293
    24
  echo
wenzelm@2293
    25
  echo "Usage: $PRG TOOL [ARGS ...]"
wenzelm@2293
    26
  echo
wenzelm@2434
    27
  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
wenzelm@2787
    28
  echo "  for more specific help."
wenzelm@2293
    29
  echo
wenzelm@2293
    30
  echo "  Availabe tools are:"
wenzelm@2293
    31
  (
wenzelm@2787
    32
    for DIR in $TOOLDIRS
wenzelm@2293
    33
    do
wenzelm@2787
    34
      cd $DIR
wenzelm@2787
    35
      echo
wenzelm@2787
    36
      for T in *
wenzelm@2787
    37
      do
wenzelm@2787
    38
        if [ -f "$T" -a -x "$T" ]; then
wenzelm@2787
    39
          DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
wenzelm@2787
    40
          echo "    $T - $DESCRLINE"
wenzelm@2787
    41
        fi
wenzelm@2787
    42
      done
wenzelm@2293
    43
    done
wenzelm@2293
    44
  )
wenzelm@2293
    45
  echo
wenzelm@2293
    46
  exit 1
wenzelm@2293
    47
}
wenzelm@2293
    48
wenzelm@2293
    49
function fail()
wenzelm@2293
    50
{
wenzelm@2344
    51
  echo "$1" >&2
wenzelm@2293
    52
  exit 2
wenzelm@2293
    53
}
wenzelm@2293
    54
wenzelm@2293
    55
wenzelm@2787
    56
## args
wenzelm@2293
    57
wenzelm@2505
    58
[ $# -lt 1 -o "$1" = "-?" ] && usage
wenzelm@2293
    59
wenzelm@2787
    60
TOOLNAME="$1"
wenzelm@2293
    61
shift
wenzelm@2293
    62
wenzelm@2787
    63
wenzelm@2787
    64
## main
wenzelm@2293
    65
wenzelm@2787
    66
for DIR in $TOOLDIRS
wenzelm@2787
    67
do
wenzelm@2787
    68
  TOOL=$DIR/$TOOLNAME
wenzelm@2787
    69
  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
wenzelm@2787
    70
done
wenzelm@2787
    71
wenzelm@2787
    72
fail "Unknown isabelle tool: $TOOLNAME"