lib/Tools/latex
changeset 8564 37a1e855390a
parent 7865 d9be8bc5624e
child 8565 3c3895e37761
     1.1 --- a/lib/Tools/latex	Fri Mar 24 08:56:48 2000 +0100
     1.2 +++ b/lib/Tools/latex	Fri Mar 24 11:52:19 2000 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    echo
     1.5    echo "  Options are:"
     1.6    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
     1.7 -  echo "                 pdf, bbl, png"
     1.8 +  echo "                 pdf, bbl, png, sty"
     1.9    echo
    1.10    echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    1.11    echo "  producing the specified output format."
    1.12 @@ -60,7 +60,7 @@
    1.13  
    1.14  ## main
    1.15  
    1.16 -# check file
    1.17 +# root file
    1.18  
    1.19  DIR=$(dirname "$FILE")
    1.20  if [ "$DIR" = . ]; then
    1.21 @@ -69,7 +69,7 @@
    1.22    FILEBASE=$DIR/$(basename "$FILE" .tex)
    1.23  fi
    1.24  
    1.25 -[ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"
    1.26 +function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" }
    1.27  
    1.28  
    1.29  # operations
    1.30 @@ -80,42 +80,62 @@
    1.31  function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    1.32  function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    1.33  
    1.34 -
    1.35 -# process file
    1.36 +function update_styles ()
    1.37 +{
    1.38 +  for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
    1.39 +  do
    1.40 +    BNAME=$(basename "$NAME")
    1.41 +    if [ ! -e "$BNAME" -o "$NAME" -nt "$BNAME" ]; then
    1.42 +      echo "updating $BNAME"
    1.43 +      cp -f "$NAME" "$BNAME"
    1.44 +    fi
    1.45 +  done
    1.46 +}
    1.47  
    1.48  case "$OUTFORMAT" in
    1.49    dvi)
    1.50 +    check_root && \
    1.51      run_latex
    1.52      RC=$?
    1.53      ;;
    1.54    dvi.gz)
    1.55 +    check_root && \
    1.56      run_latex && \
    1.57      gzip -f "$FILEBASE.dvi"
    1.58      RC=$?
    1.59      ;;
    1.60    ps)
    1.61 +    check_root && \
    1.62      run_latex && \
    1.63      run_dvips &&
    1.64      RC=$?
    1.65      ;;
    1.66    ps.gz)
    1.67 +    check_root && \
    1.68      run_latex && \
    1.69      run_dvips &&
    1.70      gzip -f "$FILEBASE.ps"
    1.71      RC=$?
    1.72      ;;
    1.73    pdf)
    1.74 +    check_root && \
    1.75      run_pdflatex
    1.76      RC=$?
    1.77      ;;
    1.78    bbl)
    1.79 +    check_root && \
    1.80      run_bibtex
    1.81      RC=$?
    1.82      ;;
    1.83    png)
    1.84 +    check_root && \
    1.85      run_thumbpdf
    1.86      RC=$?
    1.87      ;;
    1.88 +  sty)
    1.89 +    update_styles
    1.90 +    RC=$?
    1.91 +    ;;
    1.92    *)
    1.93      fail "Bad output format '$OUTFORMAT'"
    1.94      ;;