lib/Tools/document
author wenzelm
Wed Oct 13 19:43:52 1999 +0200 (1999-10-13 ago)
changeset 7857 a49a3978fe3a
parent 7814 ef6d84f16592
child 7866 3ccaa11b6df9
permissions -rwxr-xr-x
tuned usage;
     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 "  Prepare the theory session document in DIR (default '.')"
    19   echo "  producing the specified output format."
    20   echo
    21   exit 1
    22 }
    23 
    24 function fail()
    25 {
    26   echo "$1" >&2
    27   exit 2
    28 }
    29 
    30 
    31 ## process command line
    32 
    33 # options
    34 
    35 OUTFORMAT=dvi
    36 
    37 while getopts "o:" OPT
    38 do
    39   case "$OPT" in
    40     o)
    41       OUTFORMAT="$OPTARG"
    42       ;;
    43     \?)
    44       usage
    45       ;;
    46   esac
    47 done
    48 
    49 shift $(($OPTIND - 1))
    50 
    51 
    52 # args
    53 
    54 DIR="."
    55 [ $# -ge 1 ] && { DIR="$1"; shift; }
    56 
    57 [ $# -ne 0 ] && usage
    58 
    59 
    60 ## main
    61 
    62 # check format
    63 
    64 case "$OUTFORMAT" in
    65   dvi | dvi.gz | ps | ps.gz | pdf)
    66     ;;
    67   *)
    68     fail "Bad output format '$OUTFORMAT'"
    69     ;;
    70 esac
    71 
    72 
    73 # prepare document
    74 
    75 cd "$DIR" || fail "Bad directory '$DIR'"
    76 
    77 function pre_latex ()
    78 {
    79   local FMT="$1"
    80   if [ -f root.bib ]
    81   then
    82     $ISATOOL latex -o "$FMT" && \
    83     $ISATOOL latex -o bbl && \
    84     $ISATOOL latex -o "$FMT"
    85   else
    86     $ISATOOL latex -o "$FMT"
    87   fi
    88 }
    89 
    90 if [ -f IsaMakefile ]; then
    91   $ISATOOL make "$OUTFORMAT"
    92   RC=$?   #FIXME !??
    93 elif [ "$OUTFORMAT" = pdf ]; then
    94   pre_latex pdf && \
    95   $ISATOOL latex -o pdf
    96   RC=$?
    97 else
    98   pre_latex dvi && \
    99   $ISATOOL latex -o "$OUTFORMAT"
   100   RC=$?
   101 fi
   102 
   103 
   104 # install
   105 
   106 [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
   107 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"