bin/isatool
author wenzelm
Sat, 03 Feb 2001 15:21:57 +0100
changeset 11044 5873a05b4d21
parent 10555 2323ec838401
child 14981 e73f8140af78
permissions -rwxr-xr-x
use fgrep;
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
wenzelm
parents: 7971
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2293
diff changeset
     6
#
9786
wenzelm
parents: 7971
diff changeset
     7
# Isabelle tool starter -- provides settings environment
wenzelm
parents: 7971
diff changeset
     8
# and keeps your PATH name space clean.
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
     9
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    10
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    11
## settings
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    12
10511
wenzelm
parents: 9786
diff changeset
    13
PRG="$(basename "$0")"
2703
5ce1310560ff more robust handling of invocation errors;
wenzelm
parents: 2505
diff changeset
    14
10511
wenzelm
parents: 9786
diff changeset
    15
ISABELLE_HOME="$(dirname "$0")/.."
9786
wenzelm
parents: 7971
diff changeset
    16
. "$ISABELLE_HOME/lib/scripts/getsettings" || \
2936
bd33e7aae062 fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents: 2787
diff changeset
    17
  { 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
    18
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    19
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    20
## diagnostics
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    21
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    22
function usage()
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
  echo
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    25
  echo "Usage: $PRG TOOL [ARGS ...]"
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    26
  echo
2434
d3d42a2e7da2 improved usage msg;
wenzelm
parents: 2395
diff changeset
    27
  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    28
  echo "  for more specific help."
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    29
  echo
3276
f8bf5e5c1641 fixed spelling;
wenzelm
parents: 3007
diff changeset
    30
  echo "  Available tools are:"
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    31
  (
9786
wenzelm
parents: 7971
diff changeset
    32
    ORIG_IFS="$IFS"
wenzelm
parents: 7971
diff changeset
    33
    IFS=":"
wenzelm
parents: 7971
diff changeset
    34
    for DIR in $ISABELLE_TOOLS
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    35
    do
9786
wenzelm
parents: 7971
diff changeset
    36
      cd "$DIR"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    37
      echo
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    38
      for T in *
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    39
      do
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    40
        if [ -f "$T" -a -x "$T" ]; then
11044
5873a05b4d21 use fgrep;
wenzelm
parents: 10555
diff changeset
    41
          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    42
          echo "    $T - $DESCRLINE"
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    43
        fi
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    44
      done
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    45
    done
9786
wenzelm
parents: 7971
diff changeset
    46
    IFS="$ORIG_IFS"
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    47
  )
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    48
  echo
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    49
  exit 1
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    50
}
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
function fail()
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    53
{
2344
c3e1eaea4418 added -norc option;
wenzelm
parents: 2307
diff changeset
    54
  echo "$1" >&2
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    55
  exit 2
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    56
}
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    57
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    58
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    59
## args
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    60
9786
wenzelm
parents: 7971
diff changeset
    61
[ "$#" -lt 1 -o "$1" = "-?" ] && usage
2293
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
TOOLNAME="$1"
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    64
shift
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    65
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    66
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    67
## main
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    68
9786
wenzelm
parents: 7971
diff changeset
    69
ORIG_IFS="$IFS"
wenzelm
parents: 7971
diff changeset
    70
IFS=":"
wenzelm
parents: 7971
diff changeset
    71
for DIR in $ISABELLE_TOOLS
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    72
do
9786
wenzelm
parents: 7971
diff changeset
    73
  TOOL="$DIR/$TOOLNAME"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    74
  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    75
done
9786
wenzelm
parents: 7971
diff changeset
    76
IFS="$ORIG_IFS"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    77
7971
023778c8a029 tuned msg;
wenzelm
parents: 3276
diff changeset
    78
fail "Unknown Isabelle tool: $TOOLNAME"