# HG changeset patch
# User wenzelm
# Date 858094703 -3600
# Node ID 33931e1023e34206a247e28777c360b59fd85081
# Parent  b36ca42c409a08ed96b387e2a7d0cd0ef17c4cc8
tuned comments;
added ISABELLE_TOOLS support;

diff -r b36ca42c409a -r 33931e1023e3 bin/isatool
--- a/bin/isatool	Tue Mar 11 16:24:44 1997 +0100
+++ b/bin/isatool	Tue Mar 11 16:38:23 1997 +0100
@@ -3,7 +3,7 @@
 # $Id$
 #
 # Isabelle tool starter -- provides settings environment,
-#   also keeps your PATH name space clean.
+#   and keeps your PATH name space clean.
 
 
 ## settings
@@ -17,24 +17,29 @@
 
 ## diagnostics
 
+TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ")
+
 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 "  for more specific help."
   echo
   echo "  Availabe tools are:"
-  echo
   (
-    cd "$ISABELLE_HOME/lib/Tools"
-    for T in *
+    for DIR in $TOOLDIRS
     do
-      if [ -f "$T" -a -x "$T" ]; then
-        DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
-        echo "    $T - $DESCRLINE"
-      fi
+      cd $DIR
+      echo
+      for T in *
+      do
+        if [ -f "$T" -a -x "$T" ]; then
+          DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
+          echo "    $T - $DESCRLINE"
+        fi
+      done
     done
   )
   echo
@@ -48,14 +53,20 @@
 }
 
 
-## main
+## args
 
 [ $# -lt 1 -o "$1" = "-?" ] && usage
 
-TOOL_BASE="$1"
-TOOL="$ISABELLE_HOME/lib/Tools/$1"
+TOOLNAME="$1"
 shift
 
-[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
+
+## main
 
-fail "Tool not found: $TOOL_BASE"
+for DIR in $TOOLDIRS
+do
+  TOOL=$DIR/$TOOLNAME
+  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
+done
+
+fail "Unknown isabelle tool: $TOOLNAME"