diff -r c1c5652600f1 -r 749757db3ead bin/isatool
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/isatool	Mon Dec 02 18:14:32 1996 +0100
@@ -0,0 +1,59 @@
+#!/bin/bash
+#
+# Isabelle tool starter -- keeps your PATH name space clean.
+#
+# $Id$
+
+
+## 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"
+  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"