lib/Tools/document
author wenzelm
Thu Sep 27 12:24:40 2001 +0200 (2001-09-27 ago)
changeset 11581 d7bb261e3a3b
parent 10555 2323ec838401
child 11844 eb072fd9a45a
permissions -rwxr-xr-x
-v option;
     1 #!/usr/bin/env 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 "    -v           be verbose"
    22   echo
    23   echo "  Prepare the theory session document in DIR (default 'document')"
    24   echo "  producing the specified output format."
    25   echo
    26   exit 1
    27 }
    28 
    29 function fail()
    30 {
    31   echo "$1" >&2
    32   exit 2
    33 }
    34 
    35 
    36 ## process command line
    37 
    38 # options
    39 
    40 CLEAN=""
    41 OUTFORMAT=dvi
    42 VERBOSE=""
    43 
    44 while getopts "co:v" OPT
    45 do
    46   case "$OPT" in
    47     c)
    48       CLEAN=true
    49       ;;
    50     o)
    51       OUTFORMAT="$OPTARG"
    52       ;;
    53     v)
    54       VERBOSE=true
    55       ;;
    56     \?)
    57       usage
    58       ;;
    59   esac
    60 done
    61 
    62 shift $(($OPTIND - 1))
    63 
    64 
    65 # args
    66 
    67 DIR="document"
    68 [ "$#" -ge 1 ] && { DIR="$1"; shift; }
    69 
    70 [ "$#" -ne 0 ] && usage
    71 
    72 
    73 ## main
    74 
    75 # check format
    76 
    77 case "$OUTFORMAT" in
    78   dvi | dvi.gz | ps | ps.gz | pdf)
    79     ;;
    80   *)
    81     fail "Bad output format '$OUTFORMAT'"
    82     ;;
    83 esac
    84 
    85 
    86 # prepare document
    87 
    88 function pre_latex ()
    89 {
    90   local FMT="$1"
    91   [ -n "$CLEAN" ] && rm -f *.aux *.out
    92   if [ -f root.bib ]
    93   then
    94     "$ISATOOL" latex -o "$FMT" && \
    95     "$ISATOOL" latex -o bbl && \
    96     "$ISATOOL" latex -o "$FMT"
    97   else
    98     "$ISATOOL" latex -o "$FMT"
    99   fi
   100 }
   101 
   102 (
   103   cd "$DIR" || fail "Bad directory '$DIR'"
   104 
   105   [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
   106 
   107   if [ -f IsaMakefile ]; then
   108     "$ISATOOL" make "$OUTFORMAT"
   109     RC="$?"
   110   elif [ "$OUTFORMAT" = pdf ]; then
   111     pre_latex pdf && \
   112     "$ISATOOL" latex -o pdf && \
   113     { if [ -n "$ISABELLE_THUMBPDF" ]; then
   114         "$ISATOOL" latex -o png && \
   115         "$ISATOOL" latex -o pdf
   116       fi; }
   117     RC="$?"
   118   else
   119     pre_latex dvi && \
   120     "$ISATOOL" latex -o "$OUTFORMAT"
   121     RC="$?"
   122   fi
   123 
   124   if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
   125     cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" && \
   126     [ -n "$VERBOSE" ] && echo "$(cd ..; echo "Prepared $PWD/document.$OUTFORMAT")" >&2
   127   fi
   128 
   129   exit "$RC"
   130 )
   131 RC="$?"
   132 
   133 
   134 # install
   135 
   136 [ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
   137 
   138 #beware!
   139 [ -n "$CLEAN" ] && rm -rf "$DIR"
   140 
   141 exit "$RC"