lib/Tools/document
author wenzelm
Tue Feb 08 20:17:41 2000 +0100 (2000-02-08 ago)
changeset 8212 419157483fc9
parent 8211 714f164f0385
child 8217 dc3b8cdbb816
permissions -rwxr-xr-x
added -c option (beware!);
changed default DIR to 'document';
NOTE: please ignore last log entry;
     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 "    -c           clean -- remove DIR after succesful run"
    17   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
    18   echo "                 ps.gz, pdf"
    19   echo
    20   echo "  Prepare the theory session document in DIR (default 'document')"
    21   echo "  producing the specified output format."
    22   echo
    23   exit 1
    24 }
    25 
    26 function fail()
    27 {
    28   echo "$1" >&2
    29   exit 2
    30 }
    31 
    32 
    33 ## process command line
    34 
    35 # options
    36 
    37 CLEAN=""
    38 OUTFORMAT=dvi
    39 
    40 while getopts "co:" OPT
    41 do
    42   case "$OPT" in
    43     c)
    44       CLEAN=true
    45       ;;
    46     o)
    47       OUTFORMAT="$OPTARG"
    48       ;;
    49     \?)
    50       usage
    51       ;;
    52   esac
    53 done
    54 
    55 shift $(($OPTIND - 1))
    56 
    57 
    58 # args
    59 
    60 DIR="document"
    61 [ $# -ge 1 ] && { DIR="$1"; shift; }
    62 
    63 [ $# -ne 0 ] && usage
    64 
    65 
    66 ## main
    67 
    68 # check format
    69 
    70 case "$OUTFORMAT" in
    71   dvi | dvi.gz | ps | ps.gz | pdf)
    72     ;;
    73   *)
    74     fail "Bad output format '$OUTFORMAT'"
    75     ;;
    76 esac
    77 
    78 
    79 # prepare document
    80 
    81 function pre_latex ()
    82 {
    83   local FMT="$1"
    84   rm -f *.aux
    85   if [ -f root.bib ]
    86   then
    87     $ISATOOL latex -o "$FMT" && \
    88     $ISATOOL latex -o bbl && \
    89     $ISATOOL latex -o "$FMT"
    90   else
    91     $ISATOOL latex -o "$FMT"
    92   fi
    93 }
    94 
    95 (
    96   cd "$DIR" || fail "Bad directory '$DIR'"
    97 
    98   if [ -f IsaMakefile ]; then
    99     $ISATOOL make "$OUTFORMAT"
   100     RC=$?
   101   elif [ "$OUTFORMAT" = pdf ]; then
   102     pre_latex pdf && \
   103     $ISATOOL latex -o pdf && \
   104     { if [ -n "$ISABELLE_THUMBPDF" ]; then
   105         $ISATOOL latex -o png && \
   106         $ISATOOL latex -o pdf
   107       fi; }
   108     RC=$?
   109   else
   110     pre_latex dvi && \
   111     $ISATOOL latex -o "$OUTFORMAT"
   112     RC=$?
   113   fi
   114 
   115   [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
   116     cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
   117 
   118   exit $RC
   119 )
   120 RC=$?
   121 
   122 
   123 # install
   124 
   125 [ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
   126 
   127 #beware!
   128 [ -n "$CLEAN" ] && rm -rf "$DIR"
   129 
   130 exit "$RC"