lib/Tools/document
author wenzelm
Wed Nov 22 21:41:39 2000 +0100 (2000-11-22)
changeset 10511 efb3428c9879
parent 9788 df671fa2562a
child 10555 2323ec838401
permissions -rwxr-xr-x
tuned;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: prepare theory session document
     8 
     9 
    10 PRG="$(basename "$0")"
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [OPTIONS] [DIR]"
    16   echo
    17   echo "  Options are:"
    18   echo "    -c           cleanup -- be aggressive in removing old stuff"
    19   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
    20   echo "                 ps.gz, pdf"
    21   echo
    22   echo "  Prepare the theory session document in DIR (default 'document')"
    23   echo "  producing the specified output format."
    24   echo
    25   exit 1
    26 }
    27 
    28 function fail()
    29 {
    30   echo "$1" >&2
    31   exit 2
    32 }
    33 
    34 
    35 ## process command line
    36 
    37 # options
    38 
    39 CLEAN=""
    40 OUTFORMAT=dvi
    41 
    42 while getopts "co:" OPT
    43 do
    44   case "$OPT" in
    45     c)
    46       CLEAN=true
    47       ;;
    48     o)
    49       OUTFORMAT="$OPTARG"
    50       ;;
    51     \?)
    52       usage
    53       ;;
    54   esac
    55 done
    56 
    57 shift $(($OPTIND - 1))
    58 
    59 
    60 # args
    61 
    62 DIR="document"
    63 [ "$#" -ge 1 ] && { DIR="$1"; shift; }
    64 
    65 [ "$#" -ne 0 ] && usage
    66 
    67 
    68 ## main
    69 
    70 # check format
    71 
    72 case "$OUTFORMAT" in
    73   dvi | dvi.gz | ps | ps.gz | pdf)
    74     ;;
    75   *)
    76     fail "Bad output format '$OUTFORMAT'"
    77     ;;
    78 esac
    79 
    80 
    81 # prepare document
    82 
    83 function pre_latex ()
    84 {
    85   local FMT="$1"
    86   [ -n "$CLEAN" ] && rm -f *.aux *.out
    87   if [ -f root.bib ]
    88   then
    89     "$ISATOOL" latex -o "$FMT" && \
    90     "$ISATOOL" latex -o bbl && \
    91     "$ISATOOL" latex -o "$FMT"
    92   else
    93     "$ISATOOL" latex -o "$FMT"
    94   fi
    95 }
    96 
    97 (
    98   cd "$DIR" || fail "Bad directory '$DIR'"
    99 
   100   [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
   101 
   102   if [ -f IsaMakefile ]; then
   103     "$ISATOOL" make "$OUTFORMAT"
   104     RC="$?"
   105   elif [ "$OUTFORMAT" = pdf ]; then
   106     pre_latex pdf && \
   107     "$ISATOOL" latex -o pdf && \
   108     { if [ -n "$ISABELLE_THUMBPDF" ]; then
   109         "$ISATOOL" latex -o png && \
   110         "$ISATOOL" latex -o pdf
   111       fi; }
   112     RC="$?"
   113   else
   114     pre_latex dvi && \
   115     "$ISATOOL" latex -o "$OUTFORMAT"
   116     RC="$?"
   117   fi
   118 
   119   [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
   120     cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
   121 
   122   exit "$RC"
   123 )
   124 RC="$?"
   125 
   126 
   127 # install
   128 
   129 [ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
   130 
   131 #beware!
   132 [ -n "$CLEAN" ] && rm -rf "$DIR"
   133 
   134 exit "$RC"