bin/isatool
author paulson
Wed, 03 Mar 1999 10:36:24 +0100
changeset 6298 a336f80158c8
parent 3276 f8bf5e5c1641
child 7971 023778c8a029
permissions -rwxr-xr-x
expandshort
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2936
diff changeset
     1
#!/bin/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$
508d2a233dbc *** empty log message ***
wenzelm
parents: 2293
diff changeset
     4
#
2735
29434f9b95dd even more robust and user friendly invocation (no longer requieres
wenzelm
parents: 2703
diff changeset
     5
# Isabelle tool starter -- provides settings environment,
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
     6
#   and keeps your PATH name space clean.
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
     7
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
     8
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
     9
## settings
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    10
2703
5ce1310560ff more robust handling of invocation errors;
wenzelm
parents: 2505
diff changeset
    11
PRG=$(basename $0)
5ce1310560ff more robust handling of invocation errors;
wenzelm
parents: 2505
diff changeset
    12
2735
29434f9b95dd even more robust and user friendly invocation (no longer requieres
wenzelm
parents: 2703
diff changeset
    13
ISABELLE_HOME=$(dirname $0)/..
29434f9b95dd even more robust and user friendly invocation (no longer requieres
wenzelm
parents: 2703
diff changeset
    14
. $ISABELLE_HOME/lib/scripts/getsettings || \
2936
bd33e7aae062 fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents: 2787
diff changeset
    15
  { 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
    16
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    17
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    18
## diagnostics
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    19
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    20
TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ")
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    21
2293
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
  (
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    32
    for DIR in $TOOLDIRS
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    33
    do
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    34
      cd $DIR
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    35
      echo
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    36
      for T in *
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    37
      do
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    38
        if [ -f "$T" -a -x "$T" ]; then
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    39
          DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    40
          echo "    $T - $DESCRLINE"
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    41
        fi
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    42
      done
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    43
    done
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    44
  )
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    45
  echo
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    46
  exit 1
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
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    49
function fail()
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    50
{
2344
c3e1eaea4418 added -norc option;
wenzelm
parents: 2307
diff changeset
    51
  echo "$1" >&2
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    52
  exit 2
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    53
}
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
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    56
## args
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    57
2505
50abca9d4043 added -? option;
wenzelm
parents: 2434
diff changeset
    58
[ $# -lt 1 -o "$1" = "-?" ] && usage
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    59
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    60
TOOLNAME="$1"
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    61
shift
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
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    64
## main
2293
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
for DIR in $TOOLDIRS
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    67
do
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    68
  TOOL=$DIR/$TOOLNAME
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    69
  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    70
done
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    71
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    72
fail "Unknown isabelle tool: $TOOLNAME"