lib/Tools/document
author wenzelm
Sun Jan 30 13:24:41 2000 +0100 (2000-01-30 ago)
changeset 8171 f89329974d2d
parent 7866 3ccaa11b6df9
child 8211 714f164f0385
permissions -rwxr-xr-x
rm -f *.aux;
     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,"
    17   echo "                 ps.gz, pdf"
    18   echo
    19   echo "  Prepare the theory session document in DIR (default '.')"
    20   echo "  producing the specified 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   rm -f *.aux
    82   if [ -f root.bib ]
    83   then
    84     $ISATOOL latex -o "$FMT" && \
    85     $ISATOOL latex -o bbl && \
    86     $ISATOOL latex -o "$FMT"
    87   else
    88     $ISATOOL latex -o "$FMT"
    89   fi
    90 }
    91 
    92 if [ -f IsaMakefile ]; then
    93   $ISATOOL make "$OUTFORMAT"
    94   RC=$?   #FIXME !??
    95 elif [ "$OUTFORMAT" = pdf ]; then
    96   pre_latex pdf && \
    97   $ISATOOL latex -o pdf && \
    98   { if [ -n "$ISABELLE_THUMBPDF" ]; then
    99       $ISATOOL latex -o png && \
   100       $ISATOOL latex -o pdf
   101     fi; }
   102   RC=$?
   103 else
   104   pre_latex dvi && \
   105   $ISATOOL latex -o "$OUTFORMAT"
   106   RC=$?
   107 fi
   108 
   109 
   110 # install
   111 
   112 [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
   113 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"