bin/isatool
author wenzelm
Tue, 10 Jul 2007 16:45:04 +0200
changeset 23701 1716f19e7d25
parent 15967 f9163c6f69d6
permissions -rwxr-xr-x
Markup.output; removed no_state markup -- produce empty state;
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
#
15967
f9163c6f69d6 proper treatment of directory links;
wenzelm
parents: 15877
diff changeset
     6
# Isabelle tool starter.
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
     7
15843
d5bd4a18ce70 improved handling of symlinks;
wenzelm
parents: 14981
diff changeset
     8
if [ -L "$0" ]; then
d5bd4a18ce70 improved handling of symlinks;
wenzelm
parents: 14981
diff changeset
     9
  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
15967
f9163c6f69d6 proper treatment of directory links;
wenzelm
parents: 15877
diff changeset
    10
  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
15843
d5bd4a18ce70 improved handling of symlinks;
wenzelm
parents: 14981
diff changeset
    11
fi
d5bd4a18ce70 improved handling of symlinks;
wenzelm
parents: 14981
diff changeset
    12
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    13
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    14
## settings
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    15
10511
wenzelm
parents: 9786
diff changeset
    16
PRG="$(basename "$0")"
2703
5ce1310560ff more robust handling of invocation errors;
wenzelm
parents: 2505
diff changeset
    17
15967
f9163c6f69d6 proper treatment of directory links;
wenzelm
parents: 15877
diff changeset
    18
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
f9163c6f69d6 proper treatment of directory links;
wenzelm
parents: 15877
diff changeset
    19
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    20
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
## diagnostics
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
function usage()
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
  echo
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    27
  echo "Usage: $PRG TOOL [ARGS ...]"
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    28
  echo
2434
d3d42a2e7da2 improved usage msg;
wenzelm
parents: 2395
diff changeset
    29
  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    30
  echo "  for more specific help."
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    31
  echo
3276
f8bf5e5c1641 fixed spelling;
wenzelm
parents: 3007
diff changeset
    32
  echo "  Available tools are:"
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    33
  (
9786
wenzelm
parents: 7971
diff changeset
    34
    ORIG_IFS="$IFS"
wenzelm
parents: 7971
diff changeset
    35
    IFS=":"
wenzelm
parents: 7971
diff changeset
    36
    for DIR in $ISABELLE_TOOLS
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    37
    do
9786
wenzelm
parents: 7971
diff changeset
    38
      cd "$DIR"
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    39
      for T in *
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    40
      do
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    41
        if [ -f "$T" -a -x "$T" ]; then
11044
5873a05b4d21 use fgrep;
wenzelm
parents: 10555
diff changeset
    42
          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
2787
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    43
          echo "    $T - $DESCRLINE"
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    44
        fi
33931e1023e3 tuned comments;
wenzelm
parents: 2737
diff changeset
    45
      done
2293
749757db3ead isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff changeset
    46
    done
9786
wenzelm
parents: 7971
diff changeset
    47
    IFS="$ORIG_IFS"
2293
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
  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"