lib/Tools/usedir
changeset 17194 70d96933c210
parent 17050 bfb571252817
child 18321 3414557c2dda
equal deleted inserted replaced
17193:83708f724822 17194:70d96933c210
    14 {
    14 {
    15   echo
    15   echo
    16   echo "Usage: $PRG [OPTIONS] LOGIC NAME"
    16   echo "Usage: $PRG [OPTIONS] LOGIC NAME"
    17   echo
    17   echo
    18   echo "  Options are:"
    18   echo "  Options are:"
       
    19   echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
    19   echo "    -D PATH      dump generated document sources into PATH"
    20   echo "    -D PATH      dump generated document sources into PATH"
    20   echo "    -P PATH      set path for remote theory browsing information"
    21   echo "    -P PATH      set path for remote theory browsing information"
    21   echo "    -V VERSION   declare alternative document VERSION"
    22   echo "    -V VERSION   declare alternative document VERSION"
    22   echo "    -b           build mode (output heap image, using current dir)"
    23   echo "    -b           build mode (output heap image, using current dir)"
    23   echo "    -c BOOL      tell ML system to compress output image (default true)"
    24   echo "    -c BOOL      tell ML system to compress output image (default true)"
    58 
    59 
    59 ## process command line
    60 ## process command line
    60 
    61 
    61 # options
    62 # options
    62 
    63 
       
    64 COPY_DUMP="true"
    63 DUMP=""
    65 DUMP=""
    64 RPATH=""
    66 RPATH=""
    65 DOCUMENT_VERSIONS=""
    67 DOCUMENT_VERSIONS=""
    66 BUILD=""
    68 BUILD=""
    67 COMPRESS=true
    69 COMPRESS=true
    76 VERBOSE=false
    78 VERBOSE=false
    77 
    79 
    78 function getoptions()
    80 function getoptions()
    79 {
    81 {
    80   OPTIND=1
    82   OPTIND=1
    81   while getopts "D:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
    83   while getopts "C:D:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
    82   do
    84   do
    83     case "$OPT" in
    85     case "$OPT" in
       
    86       C)
       
    87         check_bool "$OPTARG"
       
    88         COPY_DUMP="$OPTARG"
       
    89         ;;
    84       D)
    90       D)
    85         DUMP="$OPTARG"
    91         DUMP="$OPTARG"
    86         ;;
    92         ;;
    87       P)
    93       P)
    88         RPATH="$OPTARG"
    94         RPATH="$OPTARG"
   201 
   207 
   202   OPT_C=""
   208   OPT_C=""
   203   [ "$COMPRESS" = true ] && OPT_C="-c"
   209   [ "$COMPRESS" = true ] && OPT_C="-c"
   204 
   210 
   205   "$ISABELLE" \
   211   "$ISABELLE" \
   206     -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \
   212     -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE;" \
   207     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   213     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   208   RC="$?"
   214   RC="$?"
   209 else
   215 else
   210   ITEM=$(basename "$LOGIC")-"$SESSION"
   216   ITEM=$(basename "$LOGIC")-"$SESSION"
   211   echo "Running $ITEM ..." >&2
   217   echo "Running $ITEM ..." >&2
   212   LOG="$LOGDIR/$ITEM"
   218   LOG="$LOGDIR/$ITEM"
   213 
   219 
   214   "$ISABELLE" \
   220   "$ISABELLE" \
   215     -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \
   221     -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE; quit();" \
   216     -r -q "$LOGIC" > "$LOG"
   222     -r -q "$LOGIC" > "$LOG"
   217   RC="$?"
   223   RC="$?"
   218   cd ..
   224   cd ..
   219 fi
   225 fi
   220 
   226