bin/isatool
author wenzelm
Sat, 20 Oct 2001 20:14:16 +0200
changeset 11842 b903d3dabbe2
parent 11044 5873a05b4d21
child 14981 e73f8140af78
permissions -rwxr-xr-x
* greatly simplified document preparation setup, including more graceful interpretation of isatool usedir -i/-d/-D options, and more instructive isatool mkdir; users should basically be able to get started with "isatool mkdir Test && isatool make"; * theory dependency graph may now be incorporated into documents; isatool usedir -g true will produce session_graph.eps/.pdf for use with \includegraphics of LaTeX;

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# Isabelle tool starter -- provides settings environment
# and 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 more specific help."
  echo
  echo "  Available tools are:"
  (
    ORIG_IFS="$IFS"
    IFS=":"
    for DIR in $ISABELLE_TOOLS
    do
      cd "$DIR"
      echo
      for T in *
      do
        if [ -f "$T" -a -x "$T" ]; then
          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
          echo "    $T - $DESCRLINE"
        fi
      done
    done
    IFS="$ORIG_IFS"
  )
  echo
  exit 1
}

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


## args

[ "$#" -lt 1 -o "$1" = "-?" ] && usage

TOOLNAME="$1"
shift


## main

ORIG_IFS="$IFS"
IFS=":"
for DIR in $ISABELLE_TOOLS
do
  TOOL="$DIR/$TOOLNAME"
  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
done
IFS="$ORIG_IFS"

fail "Unknown Isabelle tool: $TOOLNAME"