bin/isatool
author wenzelm
Thu Mar 06 12:28:17 1997 +0100 (1997-03-06)
changeset 2735 29434f9b95dd
parent 2703 5ce1310560ff
child 2737 a43320c05e84
permissions -rwxr-xr-x
even more robust and user friendly invocation (no longer requieres
absolute path names);
wenzelm@2735
     1
#!/bin/bash -x
wenzelm@2293
     2
#
wenzelm@2307
     3
# $Id$
wenzelm@2307
     4
#
wenzelm@2735
     5
# Isabelle tool starter -- provides settings environment,
wenzelm@2735
     6
#   also 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@2735
    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@2293
    20
function usage()
wenzelm@2293
    21
{
wenzelm@2293
    22
  echo
wenzelm@2293
    23
  echo "Usage: $PRG TOOL [ARGS ...]"
wenzelm@2293
    24
  echo
wenzelm@2434
    25
  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
wenzelm@2434
    26
  echo "  for specific help."
wenzelm@2293
    27
  echo
wenzelm@2293
    28
  echo "  Availabe tools are:"
wenzelm@2434
    29
  echo
wenzelm@2293
    30
  (
wenzelm@2293
    31
    cd "$ISABELLE_HOME/lib/Tools"
wenzelm@2293
    32
    for T in *
wenzelm@2293
    33
    do
wenzelm@2293
    34
      if [ -f "$T" -a -x "$T" ]; then
wenzelm@2293
    35
        DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
wenzelm@2293
    36
        echo "    $T - $DESCRLINE"
wenzelm@2293
    37
      fi
wenzelm@2293
    38
    done
wenzelm@2293
    39
  )
wenzelm@2293
    40
  echo
wenzelm@2293
    41
  exit 1
wenzelm@2293
    42
}
wenzelm@2293
    43
wenzelm@2293
    44
function fail()
wenzelm@2293
    45
{
wenzelm@2344
    46
  echo "$1" >&2
wenzelm@2293
    47
  exit 2
wenzelm@2293
    48
}
wenzelm@2293
    49
wenzelm@2293
    50
wenzelm@2293
    51
## main
wenzelm@2293
    52
wenzelm@2505
    53
[ $# -lt 1 -o "$1" = "-?" ] && usage
wenzelm@2293
    54
wenzelm@2293
    55
TOOL_BASE="$1"
wenzelm@2293
    56
TOOL="$ISABELLE_HOME/lib/Tools/$1"
wenzelm@2293
    57
shift
wenzelm@2293
    58
wenzelm@2293
    59
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
wenzelm@2293
    60
wenzelm@2293
    61
fail "Tool not found: $TOOL_BASE"