lib/Tools/document
author wenzelm
Fri Oct 08 15:03:11 1999 +0200 (1999-10-08 ago)
changeset 7793 e0676a932348
child 7814 ef6d84f16592
permissions -rwxr-xr-x
prepare theory session document;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: prepare theory session document
     6 
     7 
     8 PRG=$(basename $0)
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG [OPTIONS] [DIR]"
    14   echo
    15   echo "  Options are:"
    16   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
    17   echo
    18   echo
    19   echo "  Prepare the theory session document in DIR (default .)"
    20   echo "  producing the speficied output format."
    21   echo
    22   exit 1
    23 }
    24 
    25 function fail()
    26 {
    27   echo "$1" >&2
    28   exit 2
    29 }
    30 
    31 
    32 ## process command line
    33 
    34 # options
    35 
    36 OUTFORMAT=dvi
    37 
    38 while getopts "o:" OPT
    39 do
    40   case "$OPT" in
    41     o)
    42       OUTFORMAT="$OPTARG"
    43       ;;
    44     \?)
    45       usage
    46       ;;
    47   esac
    48 done
    49 
    50 shift $(($OPTIND - 1))
    51 
    52 
    53 # args
    54 
    55 DIR="."
    56 [ $# -ge 1 ] && { DIR="$1"; shift; }
    57 
    58 [ $# -ne 0 ] && usage
    59 
    60 
    61 ## main
    62 
    63 #prepare document
    64 
    65 cd "$DIR" || fail "Bad directory '$DIR'"
    66 
    67 if [ -f IsaMakefile ]; then
    68   $ISATOOL make "$OUTFORMAT"
    69   RC=$?   #FIXME !??
    70 elif [ "$OUTFORMAT" = pdf ]; then
    71   $ISATOOL latex -o pdf && $ISATOOL latex -o pdf
    72   RC=$?
    73 else
    74   $ISATOOL latex -o dvi && $ISATOOL latex -o "$OUTFORMAT"
    75   RC=$?
    76 fi
    77 
    78 
    79 #install
    80 
    81 [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
    82 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"