| 7793 |      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 | 
 | 
| 7814 |     63 | # check format
 | 
|  |     64 | 
 | 
|  |     65 | case "$OUTFORMAT" in
 | 
|  |     66 |   dvi | dvi.gz | ps | ps.gz | pdf)
 | 
|  |     67 |     ;;
 | 
|  |     68 |   *)
 | 
|  |     69 |     fail "Bad output format '$OUTFORMAT'"
 | 
|  |     70 |     ;;
 | 
|  |     71 | esac
 | 
|  |     72 | 
 | 
|  |     73 | 
 | 
|  |     74 | # prepare document
 | 
| 7793 |     75 | 
 | 
|  |     76 | cd "$DIR" || fail "Bad directory '$DIR'"
 | 
|  |     77 | 
 | 
| 7814 |     78 | function pre_latex ()
 | 
|  |     79 | {
 | 
|  |     80 |   local FMT="$1"
 | 
|  |     81 |   if [ -f root.bib ]
 | 
|  |     82 |   then
 | 
|  |     83 |     $ISATOOL latex -o "$FMT" && \
 | 
|  |     84 |     $ISATOOL latex -o bbl && \
 | 
|  |     85 |     $ISATOOL latex -o "$FMT"
 | 
|  |     86 |   else
 | 
|  |     87 |     $ISATOOL latex -o "$FMT"
 | 
|  |     88 |   fi
 | 
|  |     89 | }
 | 
|  |     90 | 
 | 
| 7793 |     91 | if [ -f IsaMakefile ]; then
 | 
|  |     92 |   $ISATOOL make "$OUTFORMAT"
 | 
|  |     93 |   RC=$?   #FIXME !??
 | 
|  |     94 | elif [ "$OUTFORMAT" = pdf ]; then
 | 
| 7814 |     95 |   pre_latex pdf && \
 | 
|  |     96 |   $ISATOOL latex -o pdf
 | 
| 7793 |     97 |   RC=$?
 | 
|  |     98 | else
 | 
| 7814 |     99 |   pre_latex dvi && \
 | 
|  |    100 |   $ISATOOL latex -o "$OUTFORMAT"
 | 
| 7793 |    101 |   RC=$?
 | 
|  |    102 | fi
 | 
|  |    103 | 
 | 
|  |    104 | 
 | 
| 7814 |    105 | # install
 | 
| 7793 |    106 | 
 | 
|  |    107 | [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
 | 
|  |    108 | cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
 |