lib/Tools/latex
author wenzelm
Fri Mar 24 13:47:36 2000 +0100 (2000-03-24)
changeset 8565 3c3895e37761
parent 8564 37a1e855390a
child 8568 b18540435f26
permissions -rwxr-xr-x
improved dump of styles;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: run LaTeX (and related tools)
     6 
     7 
     8 PRG=$(basename $0)
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG [OPTIONS] [FILE]"
    14   echo
    15   echo "  Options are:"
    16   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
    17   echo "                 pdf, bbl, png, sty"
    18   echo
    19   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    20   echo "  producing the specified output format."
    21   echo
    22   exit 1
    23 }
    24 
    25 function fail()
    26 {
    27   echo "$1" >&2
    28   exit 2
    29 }
    30 
    31 
    32 ## process command line
    33 
    34 # options
    35 
    36 OUTFORMAT=dvi
    37 
    38 while getopts "o:" OPT
    39 do
    40   case "$OPT" in
    41     o)
    42       OUTFORMAT="$OPTARG"
    43       ;;
    44     \?)
    45       usage
    46       ;;
    47   esac
    48 done
    49 
    50 shift $(($OPTIND - 1))
    51 
    52 
    53 # args
    54 
    55 FILE="root.tex"
    56 [ $# -ge 1 ] && { FILE="$1"; shift; }
    57 
    58 [ $# -ne 0 ] && usage
    59 
    60 
    61 ## main
    62 
    63 # root file
    64 
    65 DIR=$(dirname "$FILE")
    66 if [ "$DIR" = . ]; then
    67   FILEBASE=$(basename "$FILE" .tex)
    68 else
    69   FILEBASE=$DIR/$(basename "$FILE" .tex)
    70 fi
    71 
    72 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" }
    73 
    74 
    75 # operations
    76 
    77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    78 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    79 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    80 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    81 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    82 
    83 function update_styles ()
    84 {
    85   for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
    86   do
    87     DEST="$DIR"/$(basename "$NAME")
    88     if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
    89       echo "updating $DEST"
    90       cp -f "$NAME" "$DEST"
    91     fi
    92   done
    93 }
    94 
    95 case "$OUTFORMAT" in
    96   dvi)
    97     check_root && \
    98     run_latex
    99     RC=$?
   100     ;;
   101   dvi.gz)
   102     check_root && \
   103     run_latex && \
   104     gzip -f "$FILEBASE.dvi"
   105     RC=$?
   106     ;;
   107   ps)
   108     check_root && \
   109     run_latex && \
   110     run_dvips &&
   111     RC=$?
   112     ;;
   113   ps.gz)
   114     check_root && \
   115     run_latex && \
   116     run_dvips &&
   117     gzip -f "$FILEBASE.ps"
   118     RC=$?
   119     ;;
   120   pdf)
   121     check_root && \
   122     run_pdflatex
   123     RC=$?
   124     ;;
   125   bbl)
   126     check_root && \
   127     run_bibtex
   128     RC=$?
   129     ;;
   130   png)
   131     check_root && \
   132     run_thumbpdf
   133     RC=$?
   134     ;;
   135   sty)
   136     update_styles
   137     RC=$?
   138     ;;
   139   *)
   140     fail "Bad output format '$OUTFORMAT'"
   141     ;;
   142 esac
   143 
   144 exit $RC