bin/isatool
author wenzelm
Mon, 09 Dec 1996 16:39:53 +0100
changeset 2346 c0165f34e987
parent 2344 c3e1eaea4418
child 2395 c24a79fe3651
permissions -rwxr-xr-x
getplatform - bash source script to augment current env;

#!/bin/bash -norc
#
# $Id$
#
# Isabelle tool starter -- keeps your PATH name space clean.


## settings

ISABELLE_HOME=$(dirname $(dirname $0))
. $ISABELLE_HOME/lib/scripts/getsettings


## diagnostics

PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG TOOL [ARGS ...]"
  echo
  echo "  Start Isabelle utility program TOOL with ARGS."
  echo
  echo "  Availabe tools are:"
  (
    cd "$ISABELLE_HOME/lib/Tools"
    for T in *
    do
      if [ -f "$T" -a -x "$T" ]; then
        DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
        echo "    $T - $DESCRLINE"
      fi
    done
  )
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## main

[ $# -lt 1 ] && usage

TOOL_BASE="$1"
TOOL="$ISABELLE_HOME/lib/Tools/$1"
shift

[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"

fail "Tool not found: $TOOL_BASE"