lib/Tools/document
changeset 7793 e0676a932348
child 7814 ef6d84f16592
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/Tools/document	Fri Oct 08 15:03:11 1999 +0200
     1.3 @@ -0,0 +1,82 @@
     1.4 +#!/bin/bash
     1.5 +#
     1.6 +# $Id$
     1.7 +#
     1.8 +# DESCRIPTION: prepare theory session document
     1.9 +
    1.10 +
    1.11 +PRG=$(basename $0)
    1.12 +
    1.13 +function usage()
    1.14 +{
    1.15 +  echo
    1.16 +  echo "Usage: $PRG [OPTIONS] [DIR]"
    1.17 +  echo
    1.18 +  echo "  Options are:"
    1.19 +  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
    1.20 +  echo
    1.21 +  echo
    1.22 +  echo "  Prepare the theory session document in DIR (default .)"
    1.23 +  echo "  producing the speficied output format."
    1.24 +  echo
    1.25 +  exit 1
    1.26 +}
    1.27 +
    1.28 +function fail()
    1.29 +{
    1.30 +  echo "$1" >&2
    1.31 +  exit 2
    1.32 +}
    1.33 +
    1.34 +
    1.35 +## process command line
    1.36 +
    1.37 +# options
    1.38 +
    1.39 +OUTFORMAT=dvi
    1.40 +
    1.41 +while getopts "o:" OPT
    1.42 +do
    1.43 +  case "$OPT" in
    1.44 +    o)
    1.45 +      OUTFORMAT="$OPTARG"
    1.46 +      ;;
    1.47 +    \?)
    1.48 +      usage
    1.49 +      ;;
    1.50 +  esac
    1.51 +done
    1.52 +
    1.53 +shift $(($OPTIND - 1))
    1.54 +
    1.55 +
    1.56 +# args
    1.57 +
    1.58 +DIR="."
    1.59 +[ $# -ge 1 ] && { DIR="$1"; shift; }
    1.60 +
    1.61 +[ $# -ne 0 ] && usage
    1.62 +
    1.63 +
    1.64 +## main
    1.65 +
    1.66 +#prepare document
    1.67 +
    1.68 +cd "$DIR" || fail "Bad directory '$DIR'"
    1.69 +
    1.70 +if [ -f IsaMakefile ]; then
    1.71 +  $ISATOOL make "$OUTFORMAT"
    1.72 +  RC=$?   #FIXME !??
    1.73 +elif [ "$OUTFORMAT" = pdf ]; then
    1.74 +  $ISATOOL latex -o pdf && $ISATOOL latex -o pdf
    1.75 +  RC=$?
    1.76 +else
    1.77 +  $ISATOOL latex -o dvi && $ISATOOL latex -o "$OUTFORMAT"
    1.78 +  RC=$?
    1.79 +fi
    1.80 +
    1.81 +
    1.82 +#install
    1.83 +
    1.84 +[ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
    1.85 +cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"