# HG changeset patch
# User wenzelm
# Date 1116316720 -7200
# Node ID f9163c6f69d60f7af7874a0829685fbccc293f38
# Parent  73cf5ef8ed20575b303debb26f6e56eaa4ec706e
proper treatment of directory links;
tuned;

diff -r 73cf5ef8ed20 -r f9163c6f69d6 bin/isabelle
--- a/bin/isabelle	Tue May 17 01:24:19 2005 +0200
+++ b/bin/isabelle	Tue May 17 09:58:40 2005 +0200
@@ -7,10 +7,10 @@
 
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
-  exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
-THIS=$(cd "$(dirname "$0")"; pwd)
+THIS=$(cd "$(dirname "$0")"; pwd -P)
 NAME="$(basename "$0")"
 
 case "$NAME" in
diff -r 73cf5ef8ed20 -r f9163c6f69d6 bin/isabelle-interface
--- a/bin/isabelle-interface	Tue May 17 01:24:19 2005 +0200
+++ b/bin/isabelle-interface	Tue May 17 09:58:40 2005 +0200
@@ -7,7 +7,7 @@
 
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
-  exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
 
@@ -15,9 +15,8 @@
 
 PRG="$(basename "$0")"
 
-ISABELLE_HOME="$(dirname "$0")/.."
-. "$ISABELLE_HOME/lib/scripts/getsettings" || \
-  { echo "$PRG probably not called from its original place!"; exit 2; }
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
 
 ## diagnostics
diff -r 73cf5ef8ed20 -r f9163c6f69d6 bin/isabelle-process
--- a/bin/isabelle-process	Tue May 17 01:24:19 2005 +0200
+++ b/bin/isabelle-process	Tue May 17 09:58:40 2005 +0200
@@ -7,7 +7,7 @@
 
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
-  exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
 
@@ -15,9 +15,8 @@
 
 PRG="$(basename "$0")"
 
-ISABELLE_HOME="$(dirname "$0")/.."
-. "$ISABELLE_HOME/lib/scripts/getsettings" || \
-  { echo "$PRG probably not called from its original place!"; exit 2; }
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
 
 ## diagnostics
diff -r 73cf5ef8ed20 -r f9163c6f69d6 bin/isatool
--- a/bin/isatool	Tue May 17 01:24:19 2005 +0200
+++ b/bin/isatool	Tue May 17 09:58:40 2005 +0200
@@ -3,12 +3,11 @@
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
 #
-# Isabelle tool starter -- provides settings environment
-# and keeps your PATH name space clean.
+# Isabelle tool starter.
 
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
-  exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
 
@@ -16,9 +15,8 @@
 
 PRG="$(basename "$0")"
 
-ISABELLE_HOME="$(dirname "$0")/.."
-. "$ISABELLE_HOME/lib/scripts/getsettings" || \
-  { echo "$PRG probably not called from its original place!"; exit 2; }
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
 
 ## diagnostics
@@ -38,7 +36,6 @@
     for DIR in $ISABELLE_TOOLS
     do
       cd "$DIR"
-      echo
       for T in *
       do
         if [ -f "$T" -a -x "$T" ]; then
@@ -49,7 +46,6 @@
     done
     IFS="$ORIG_IFS"
   )
-  echo
   exit 1
 }
 
diff -r 73cf5ef8ed20 -r f9163c6f69d6 build
--- a/build	Tue May 17 01:24:19 2005 +0200
+++ b/build	Tue May 17 09:58:40 2005 +0200
@@ -7,7 +7,7 @@
 
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
-  exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
 
@@ -18,13 +18,12 @@
 
 ## settings
 
-PRG="$(basename "$0")"
-
 export THIS_IS_ISABELLE_BUILD=true
 
-ISABELLE_HOME="$(dirname "$0")"
-. "$ISABELLE_HOME/lib/scripts/getsettings" || \
-  { echo "$PRG probably not called from its original place!"; exit 2; }
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
 
 ## diagnostics