bin/isatool
author wenzelm
Thu, 28 Apr 2005 21:36:25 +0200
changeset 15877 c9efc3e3fd44
parent 15843 d5bd4a18ce70
child 15967 f9163c6f69d6
permissions -rwxr-xr-x
make symlink handling compatible with whitespaces
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env bash
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
     2
#
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2293
diff changeset
     3
# $Id$
9786
wenzelm
parents: 7971
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2293
diff changeset
     5
#
9786
wenzelm
parents: 7971
diff changeset
     6
# Isabelle tool starter -- provides settings environment
wenzelm
parents: 7971
diff changeset
     7
# and keeps your PATH name space clean.
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
     8
15843
d5bd4a18ce70 improved handling of symlinks;
wenzelm
parents: 14981
diff changeset
     9
if [ -L "$0" ]; then
d5bd4a18ce70 improved handling of symlinks;
wenzelm
parents: 14981
diff changeset
    10
  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
15877
c9efc3e3fd44 make symlink handling compatible with whitespaces
wenzelm
parents: 15843
diff changeset
    11
  exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
15843
d5bd4a18ce70 improved handling of symlinks;
wenzelm
parents: 14981
diff changeset
    12
fi
d5bd4a18ce70 improved handling of symlinks;
wenzelm
parents: 14981
diff changeset
    13
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    14
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    15
## settings
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    16
10511
wenzelm
parents: 9786
diff changeset
    17
PRG="$(basename "$0")"
2703
5ce1310560ff more robust handling of invocation errors;
wenzelm
parents: 2505
diff changeset
    18
10511
wenzelm
parents: 9786
diff changeset
    19
ISABELLE_HOME="$(dirname "$0")/.."
9786
wenzelm
parents: 7971
diff changeset
    20
. "$ISABELLE_HOME/lib/scripts/getsettings" || \
2936
bd33e7aae062 fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents: 2787
diff changeset
    21
  { echo "$PRG probably not called from its original place!"; exit 2; }
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    22
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    23
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    24
## diagnostics
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    25
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    26
function usage()
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    27
{
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    28
  echo
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    29
  echo "Usage: $PRG TOOL [ARGS ...]"
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    30
  echo
2434
d3d42a2e7da2 improved usage msg;
wenzelm
parents: 2395
diff changeset
    31
  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    32
  echo "  for more specific help."
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    33
  echo
3276
f8bf5e5c1641 fixed spelling;
wenzelm
parents: 3007
diff changeset
    34
  echo "  Available tools are:"
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    35
  (
9786
wenzelm
parents: 7971
diff changeset
    36
    ORIG_IFS="$IFS"
wenzelm
parents: 7971
diff changeset
    37
    IFS=":"
wenzelm
parents: 7971
diff changeset
    38
    for DIR in $ISABELLE_TOOLS
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    39
    do
9786
wenzelm
parents: 7971
diff changeset
    40
      cd "$DIR"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    41
      echo
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    42
      for T in *
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    43
      do
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    44
        if [ -f "$T" -a -x "$T" ]; then
11044
5873a05b4d21 use fgrep;
wenzelm
parents: 10555
diff changeset
    45
          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    46
          echo "    $T - $DESCRLINE"
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    47
        fi
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    48
      done
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    49
    done
9786
wenzelm
parents: 7971
diff changeset
    50
    IFS="$ORIG_IFS"
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    51
  )
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    52
  echo
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    53
  exit 1
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    54
}
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    55
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    56
function fail()
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    57
{
2344
c3e1eaea4418 added -norc option;
wenzelm
parents: 2307
diff changeset
    58
  echo "$1" >&2
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    59
  exit 2
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    60
}
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    61
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    62
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    63
## args
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    64
9786
wenzelm
parents: 7971
diff changeset
    65
[ "$#" -lt 1 -o "$1" = "-?" ] && usage
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    66
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    67
TOOLNAME="$1"
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    68
shift
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    69
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    70
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    71
## main
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    72
9786
wenzelm
parents: 7971
diff changeset
    73
ORIG_IFS="$IFS"
wenzelm
parents: 7971
diff changeset
    74
IFS=":"
wenzelm
parents: 7971
diff changeset
    75
for DIR in $ISABELLE_TOOLS
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    76
do
9786
wenzelm
parents: 7971
diff changeset
    77
  TOOL="$DIR/$TOOLNAME"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    78
  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    79
done
9786
wenzelm
parents: 7971
diff changeset
    80
IFS="$ORIG_IFS"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    81
7971
023778c8a029 tuned msg;
wenzelm
parents: 3276
diff changeset
    82
fail "Unknown Isabelle tool: $TOOLNAME"