lib/Tools/document
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21 ago)
changeset 14981 e73f8140af78
parent 14936 a13d5118f628
child 17049 ee573216713a
permissions -rwxr-xr-x
Merged in license change from Isabelle2004
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 #
     6 # DESCRIPTION: prepare theory session document
     7 
     8 
     9 PRG="$(basename "$0")"
    10 
    11 function usage()
    12 {
    13   echo
    14   echo "Usage: $PRG [OPTIONS] [DIR]"
    15   echo
    16   echo "  Options are:"
    17   echo "    -c           cleanup -- be aggressive in removing old stuff"
    18   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
    19   echo "                 ps.gz, pdf"
    20   echo
    21   echo "  Prepare the theory session document in DIR (default 'document')"
    22   echo "  producing the specified output format."
    23   echo
    24   exit 1
    25 }
    26 
    27 function fail()
    28 {
    29   echo "$1" >&2
    30   exit 2
    31 }
    32 
    33 
    34 ## process command line
    35 
    36 # options
    37 
    38 CLEAN=""
    39 OUTFORMAT=dvi
    40 
    41 while getopts "co:" OPT
    42 do
    43   case "$OPT" in
    44     c)
    45       CLEAN=true
    46       ;;
    47     o)
    48       OUTFORMAT="$OPTARG"
    49       ;;
    50     \?)
    51       usage
    52       ;;
    53   esac
    54 done
    55 
    56 shift $(($OPTIND - 1))
    57 
    58 
    59 # args
    60 
    61 DIR="document"
    62 [ "$#" -ge 1 ] && { DIR="$1"; shift; }
    63 
    64 [ "$#" -ne 0 ] && usage
    65 
    66 
    67 ## main
    68 
    69 # check format
    70 
    71 case "$OUTFORMAT" in
    72   dvi | dvi.gz | ps | ps.gz | pdf)
    73     ;;
    74   *)
    75     fail "Bad output format '$OUTFORMAT'"
    76     ;;
    77 esac
    78 
    79 
    80 # prepare document
    81 
    82 function pre_latex ()
    83 {
    84   local FMT="$1"
    85   [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
    86   "$ISATOOL" latex -o sty && \
    87   "$ISATOOL" latex -o "$FMT" && \
    88   { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
    89   { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \
    90   "$ISATOOL" latex -o "$FMT"
    91 }
    92 
    93 (
    94   cd "$DIR" || fail "Bad directory '$DIR'"
    95 
    96   [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
    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   if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
   116     cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
   117   fi
   118 
   119   exit "$RC"
   120 )
   121 RC="$?"
   122 
   123 
   124 # install
   125 
   126 [ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
   127 
   128 #beware!
   129 [ -n "$CLEAN" ] && rm -rf "$DIR"
   130 
   131 exit "$RC"