bin/isatool

The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac
does not recognize eta-equality. But making it do so is costly

#!/bin/bash -norc
#
# $Id$
#
# Isabelle tool starter -- provides settings environment,
#   also keeps your PATH name space clean.


## settings

PRG=$(basename $0)

ISABELLE_HOME=$(dirname $0)/..
. $ISABELLE_HOME/lib/scripts/getsettings || \
  { echo "$PRG probably not called from its original place!"; exit 2 }


## diagnostics

function usage()
{
  echo
  echo "Usage: $PRG TOOL [ARGS ...]"
  echo
  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
  echo "  for specific help."
  echo
  echo "  Availabe tools are:"
  echo
  (
    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 -o "$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"