lib/Tools/latex
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: run LaTeX (and related tools)
     8 
     9 
    10 PRG="$(basename "$0")"
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [OPTIONS] [FILE]"
    16   echo
    17   echo "  Options are:"
    18   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
    19   echo "                 pdf, bbl, png, sty"
    20   echo
    21   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    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 OUTFORMAT=dvi
    39 
    40 while getopts "o:" OPT
    41 do
    42   case "$OPT" in
    43     o)
    44       OUTFORMAT="$OPTARG"
    45       ;;
    46     \?)
    47       usage
    48       ;;
    49   esac
    50 done
    51 
    52 shift $(($OPTIND - 1))
    53 
    54 
    55 # args
    56 
    57 FILE="root.tex"
    58 [ "$#" -ge 1 ] && { FILE="$1"; shift; }
    59 
    60 [ "$#" -ne 0 ] && usage
    61 
    62 
    63 ## main
    64 
    65 # root file
    66 
    67 DIR=$(dirname "$FILE")
    68 FILEBASE=$(basename "$FILE" .tex)
    69 [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
    70 
    71 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
    72 
    73 
    74 # operations
    75 
    76 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    77 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    78 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    79 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    80 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    81 
    82 function update_styles ()
    83 {
    84   for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty
    85   do
    86     DEST="$DIR"/$(basename "$NAME")
    87     if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
    88       echo "updating $DEST"
    89       cp -f "$NAME" "$DEST"
    90     fi
    91   done
    92 }
    93 
    94 case "$OUTFORMAT" in
    95   dvi)
    96     check_root && \
    97     run_latex
    98     RC="$?"
    99     ;;
   100   dvi.gz)
   101     check_root && \
   102     run_latex && \
   103     gzip -f "$FILEBASE.dvi"
   104     RC="$?"
   105     ;;
   106   ps)
   107     check_root && \
   108     run_latex && \
   109     run_dvips &&
   110     RC="$?"
   111     ;;
   112   ps.gz)
   113     check_root && \
   114     run_latex && \
   115     run_dvips &&
   116     gzip -f "$FILEBASE.ps"
   117     RC="$?"
   118     ;;
   119   pdf)
   120     check_root && \
   121     run_pdflatex
   122     RC="$?"
   123     ;;
   124   bbl)
   125     check_root && \
   126     run_bibtex
   127     RC="$?"
   128     ;;
   129   png)
   130     check_root && \
   131     run_thumbpdf
   132     RC="$?"
   133     ;;
   134   sty)
   135     update_styles
   136     RC="$?"
   137     ;;
   138   *)
   139     fail "Bad output format '$OUTFORMAT'"
   140     ;;
   141 esac
   142 
   143 exit "$RC"