rename -p to -P;
authorwenzelm
Tue Feb 08 20:14:58 2000 +0100 (2000-02-08 ago)
changeset 8211714f164f0385
parent 8210 ca3997312f47
child 8212 419157483fc9
rename -p to -P;
fixed target name: LOGIC-NAME;
lib/Tools/document
lib/Tools/mkdir
     1.1 --- a/lib/Tools/document	Tue Feb 08 20:14:09 2000 +0100
     1.2 +++ b/lib/Tools/document	Tue Feb 08 20:14:58 2000 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -#!/bin/bash
     1.5 +#!/bin/bash -x
     1.6  #
     1.7  # $Id$
     1.8  #
     1.9 @@ -13,10 +13,11 @@
    1.10    echo "Usage: $PRG [OPTIONS] [DIR]"
    1.11    echo
    1.12    echo "  Options are:"
    1.13 +  echo "    -c           clean -- remove DIR after succesful run"
    1.14    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
    1.15    echo "                 ps.gz, pdf"
    1.16    echo
    1.17 -  echo "  Prepare the theory session document in DIR (default '.')"
    1.18 +  echo "  Prepare the theory session document in DIR (default 'document')"
    1.19    echo "  producing the specified output format."
    1.20    echo
    1.21    exit 1
    1.22 @@ -33,11 +34,15 @@
    1.23  
    1.24  # options
    1.25  
    1.26 +CLEAN=""
    1.27  OUTFORMAT=dvi
    1.28  
    1.29 -while getopts "o:" OPT
    1.30 +while getopts "co:" OPT
    1.31  do
    1.32    case "$OPT" in
    1.33 +    c)
    1.34 +      CLEAN=true
    1.35 +      ;;
    1.36      o)
    1.37        OUTFORMAT="$OPTARG"
    1.38        ;;
    1.39 @@ -52,7 +57,7 @@
    1.40  
    1.41  # args
    1.42  
    1.43 -DIR="."
    1.44 +DIR="document"
    1.45  [ $# -ge 1 ] && { DIR="$1"; shift; }
    1.46  
    1.47  [ $# -ne 0 ] && usage
    1.48 @@ -73,8 +78,6 @@
    1.49  
    1.50  # prepare document
    1.51  
    1.52 -cd "$DIR" || fail "Bad directory '$DIR'"
    1.53 -
    1.54  function pre_latex ()
    1.55  {
    1.56    local FMT="$1"
    1.57 @@ -89,25 +92,39 @@
    1.58    fi
    1.59  }
    1.60  
    1.61 -if [ -f IsaMakefile ]; then
    1.62 -  $ISATOOL make "$OUTFORMAT"
    1.63 -  RC=$?   #FIXME !??
    1.64 -elif [ "$OUTFORMAT" = pdf ]; then
    1.65 -  pre_latex pdf && \
    1.66 -  $ISATOOL latex -o pdf && \
    1.67 -  { if [ -n "$ISABELLE_THUMBPDF" ]; then
    1.68 -      $ISATOOL latex -o png && \
    1.69 -      $ISATOOL latex -o pdf
    1.70 -    fi; }
    1.71 -  RC=$?
    1.72 -else
    1.73 -  pre_latex dvi && \
    1.74 -  $ISATOOL latex -o "$OUTFORMAT"
    1.75 -  RC=$?
    1.76 -fi
    1.77 +(
    1.78 +  cd "$DIR" || fail "Bad directory '$DIR'"
    1.79 +
    1.80 +  if [ -f IsaMakefile ]; then
    1.81 +    $ISATOOL make "$OUTFORMAT"
    1.82 +    RC=$?
    1.83 +  elif [ "$OUTFORMAT" = pdf ]; then
    1.84 +    pre_latex pdf && \
    1.85 +    $ISATOOL latex -o pdf && \
    1.86 +    { if [ -n "$ISABELLE_THUMBPDF" ]; then
    1.87 +        $ISATOOL latex -o png && \
    1.88 +        $ISATOOL latex -o pdf
    1.89 +      fi; }
    1.90 +    RC=$?
    1.91 +  else
    1.92 +    pre_latex dvi && \
    1.93 +    $ISATOOL latex -o "$OUTFORMAT"
    1.94 +    RC=$?
    1.95 +  fi
    1.96 +
    1.97 +  [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
    1.98 +    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
    1.99 +
   1.100 +  exit $RC
   1.101 +)
   1.102 +RC=$?
   1.103  
   1.104  
   1.105  # install
   1.106  
   1.107 -[ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
   1.108 -cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
   1.109 +[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
   1.110 +
   1.111 +#beware!
   1.112 +[ -n "$CLEAN" ] && rm -rf "$DIR"
   1.113 +
   1.114 +exit "$RC"
     2.1 --- a/lib/Tools/mkdir	Tue Feb 08 20:14:09 2000 +0100
     2.2 +++ b/lib/Tools/mkdir	Tue Feb 08 20:14:58 2000 +0100
     2.3 @@ -16,9 +16,9 @@
     2.4    echo
     2.5    echo "  Options are:"
     2.6    echo "    -I FILE      alternative IsaMakefile output"
     2.7 +  echo "    -P           include parent logic target"
     2.8    echo "    -b           setup build mode (session outputs heap image)"
     2.9    echo "    -d           setup document"
    2.10 -  echo "    -p           include parent logic target"
    2.11    echo
    2.12    echo "  Prepare session directory, including IsaMakefile, document etc."
    2.13    echo "  with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
    2.14 @@ -38,25 +38,25 @@
    2.15  # options
    2.16  
    2.17  ISAMAKEFILE="IsaMakefile"
    2.18 +PARENT=""
    2.19  BUILD=""
    2.20  DOCUMENT=""
    2.21 -PARENT=""
    2.22  
    2.23 -while getopts "I:bdp" OPT
    2.24 +while getopts "I:Pbd" OPT
    2.25  do
    2.26    case "$OPT" in
    2.27      I)
    2.28        ISAMAKEFILE="$OPTARG"
    2.29        ;;
    2.30 +    P)
    2.31 +      PARENT=true
    2.32 +      ;;
    2.33      b)
    2.34        BUILD=true
    2.35        ;;
    2.36      d)
    2.37        DOCUMENT=true
    2.38        ;;
    2.39 -    p)
    2.40 -      PARENT=true
    2.41 -      ;;
    2.42      \?)
    2.43        usage
    2.44        ;;
    2.45 @@ -95,7 +95,7 @@
    2.46  else
    2.47    IMAGES=""
    2.48    TEST="$NAME"
    2.49 -  TARGET="\$(LOG)/$NAME.gz"
    2.50 +  TARGET="\$(LOG)/$LOGIC-$NAME.gz"
    2.51    USEDIR="\$(USEDIR)"
    2.52  fi
    2.53