lib/Tools/document
changeset 8211 714f164f0385
parent 8171 f89329974d2d
child 8212 419157483fc9
     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"