lib/Tools/document
author wenzelm
Sat Oct 09 23:16:31 1999 +0200 (1999-10-09)
changeset 7814 ef6d84f16592
parent 7793 e0676a932348
child 7857 a49a3978fe3a
permissions -rwxr-xr-x
check format;
support bibtex;
     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 # 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
    75 
    76 cd "$DIR" || fail "Bad directory '$DIR'"
    77 
    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 
    91 if [ -f IsaMakefile ]; then
    92   $ISATOOL make "$OUTFORMAT"
    93   RC=$?   #FIXME !??
    94 elif [ "$OUTFORMAT" = pdf ]; then
    95   pre_latex pdf && \
    96   $ISATOOL latex -o pdf
    97   RC=$?
    98 else
    99   pre_latex dvi && \
   100   $ISATOOL latex -o "$OUTFORMAT"
   101   RC=$?
   102 fi
   103 
   104 
   105 # install
   106 
   107 [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
   108 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"