# HG changeset patch
# User wenzelm
# Date 949766338 -3600
# Node ID baab8e487fadad767f47bdf0f3a4efca715eb29e
# Parent  ecb9decd38ac79066fe4f2e3155da73348ffe75c
-D PATH: dump generated document sources into PATH;

diff -r ecb9decd38ac -r baab8e487fad lib/Tools/usedir
--- a/lib/Tools/usedir	Sat Feb 05 16:57:02 2000 +0100
+++ b/lib/Tools/usedir	Sat Feb 05 16:58:58 2000 +0100
@@ -15,6 +15,7 @@
   echo "Usage: $PRG LOGIC NAME"
   echo
   echo "  Options are:"
+  echo "    -D PATH      dump generated document sources into PATH"
   echo "    -P PATH      set path for remote theory browsing information"
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -d FORMAT    build document as FORMAT (default false)"
@@ -36,19 +37,26 @@
 
 # options
 
+DUMP=""
+RPATH=""
 BUILD=""
 DOCUMENT=false
 INFO=false
 RESET=false
 SESSION=""
-RPATH=""
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "P:bc:d:i:rs:" OPT
+  while getopts "D:P:bc:d:i:rs:" OPT
   do
     case "$OPT" in
+      D)
+        DUMP="$OPTARG"
+        ;;
+      P)
+        RPATH="$OPTARG"
+        ;;
       b)
         BUILD=true
         ;;
@@ -64,9 +72,6 @@
       s)
         SESSION="$OPTARG"
         ;;
-      P)
-        RPATH="$OPTARG"
-        ;;
       \?)
         usage
         ;;
@@ -135,7 +140,7 @@
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
-    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\";" \
+    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
     -q -w $LOGIC $NAME > $LOG 2>&1
   RC=$?
 else
@@ -144,7 +149,7 @@
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
-    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\"; quit();" \
+    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
     -r -q $LOGIC > $LOG 2>&1
   RC=$?
   cd ..