# HG changeset patch
# User wenzelm
# Date 918059417 -3600
# Node ID 974310f9ca7d8910c7b87d462fafef9ba771c99b
# Parent  43d0efafa025d43406c97e348b4c990f09e8c4d1
Session.init;

diff -r 43d0efafa025 -r 974310f9ca7d lib/Tools/usedir
--- a/lib/Tools/usedir	Wed Feb 03 17:29:48 1999 +0100
+++ b/lib/Tools/usedir	Wed Feb 03 17:30:17 1999 +0100
@@ -15,9 +15,10 @@
   echo "Usage: $PRG LOGIC NAME"
   echo
   echo "  Options are:"
-  echo "    -b           build mode (output heap image, use dir \".\")"
+  echo "    -b           build mode (output heap image, using current dir)"
   echo "    -i BOOL      generate theory browsing information,"
   echo "                 i.e. HTML / graph data (default false)"
+  echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
   echo
   echo "  Build object-logic or run examples. Also creates browsing"
@@ -33,12 +34,13 @@
 
 BUILD=""
 INFO=false
+RESET=false
 SESSION=""
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "bi:s:" OPT
+  while getopts "bi:rs:" OPT
   do
     case "$OPT" in
       b)
@@ -47,6 +49,9 @@
       i)
         INFO="$OPTARG"
         ;;
+      r)
+        RESET=true
+        ;;
       s)
         SESSION="$OPTARG"
         ;;
@@ -112,16 +117,18 @@
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
-    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; Context.add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
+    -e "Session.use_dir $RESET $INFO \"$SESSION\";" \
     -q -w $LOGIC $NAME > $LOG 2>&1
 else
   ITEM=$(basename $LOGIC)-"$SESSION"
   echo -n "Running $ITEM ... "
   LOG="$LOGDIR/$ITEM"
 
+  cd "$NAME"
   $ISABELLE \
-    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; Context.add_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
+    -e "Session.use_dir $RESET $INFO \"$SESSION\"; quit();" \
     -r -q $LOGIC > $LOG 2>&1
+  cd ..
 fi
 
 RC=$?