-D PATH: dump generated document sources into PATH;
authorwenzelm
Sat Feb 05 16:58:58 2000 +0100 (2000-02-05)
changeset 8197baab8e487fad
parent 8196 ecb9decd38ac
child 8198 73a5877ca517
-D PATH: dump generated document sources into PATH;
lib/Tools/usedir
     1.1 --- a/lib/Tools/usedir	Sat Feb 05 16:57:02 2000 +0100
     1.2 +++ b/lib/Tools/usedir	Sat Feb 05 16:58:58 2000 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    echo "Usage: $PRG LOGIC NAME"
     1.5    echo
     1.6    echo "  Options are:"
     1.7 +  echo "    -D PATH      dump generated document sources into PATH"
     1.8    echo "    -P PATH      set path for remote theory browsing information"
     1.9    echo "    -b           build mode (output heap image, using current dir)"
    1.10    echo "    -d FORMAT    build document as FORMAT (default false)"
    1.11 @@ -36,19 +37,26 @@
    1.12  
    1.13  # options
    1.14  
    1.15 +DUMP=""
    1.16 +RPATH=""
    1.17  BUILD=""
    1.18  DOCUMENT=false
    1.19  INFO=false
    1.20  RESET=false
    1.21  SESSION=""
    1.22 -RPATH=""
    1.23  
    1.24  function getoptions()
    1.25  {
    1.26    OPTIND=1
    1.27 -  while getopts "P:bc:d:i:rs:" OPT
    1.28 +  while getopts "D:P:bc:d:i:rs:" OPT
    1.29    do
    1.30      case "$OPT" in
    1.31 +      D)
    1.32 +        DUMP="$OPTARG"
    1.33 +        ;;
    1.34 +      P)
    1.35 +        RPATH="$OPTARG"
    1.36 +        ;;
    1.37        b)
    1.38          BUILD=true
    1.39          ;;
    1.40 @@ -64,9 +72,6 @@
    1.41        s)
    1.42          SESSION="$OPTARG"
    1.43          ;;
    1.44 -      P)
    1.45 -        RPATH="$OPTARG"
    1.46 -        ;;
    1.47        \?)
    1.48          usage
    1.49          ;;
    1.50 @@ -135,7 +140,7 @@
    1.51    LOG="$LOGDIR/$ITEM"
    1.52  
    1.53    $ISABELLE \
    1.54 -    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\";" \
    1.55 +    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
    1.56      -q -w $LOGIC $NAME > $LOG 2>&1
    1.57    RC=$?
    1.58  else
    1.59 @@ -144,7 +149,7 @@
    1.60    LOG="$LOGDIR/$ITEM"
    1.61  
    1.62    $ISABELLE \
    1.63 -    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\"; quit();" \
    1.64 +    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
    1.65      -r -q $LOGIC > $LOG 2>&1
    1.66    RC=$?
    1.67    cd ..