# HG changeset patch
# User wenzelm
# Date 953895139 -3600
# Node ID 37a1e855390ad6ed44996c6481862f15c47b190d
# Parent  2746bc9a7ef266aa672f574797e3329469084d84
-o sty;

diff -r 2746bc9a7ef2 -r 37a1e855390a lib/Tools/latex
--- a/lib/Tools/latex	Fri Mar 24 08:56:48 2000 +0100
+++ b/lib/Tools/latex	Fri Mar 24 11:52:19 2000 +0100
@@ -14,7 +14,7 @@
   echo
   echo "  Options are:"
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
-  echo "                 pdf, bbl, png"
+  echo "                 pdf, bbl, png, sty"
   echo
   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
   echo "  producing the specified output format."
@@ -60,7 +60,7 @@
 
 ## main
 
-# check file
+# root file
 
 DIR=$(dirname "$FILE")
 if [ "$DIR" = . ]; then
@@ -69,7 +69,7 @@
   FILEBASE=$DIR/$(basename "$FILE" .tex)
 fi
 
-[ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"
+function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" }
 
 
 # operations
@@ -80,42 +80,62 @@
 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
 
-
-# process file
+function update_styles ()
+{
+  for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
+  do
+    BNAME=$(basename "$NAME")
+    if [ ! -e "$BNAME" -o "$NAME" -nt "$BNAME" ]; then
+      echo "updating $BNAME"
+      cp -f "$NAME" "$BNAME"
+    fi
+  done
+}
 
 case "$OUTFORMAT" in
   dvi)
+    check_root && \
     run_latex
     RC=$?
     ;;
   dvi.gz)
+    check_root && \
     run_latex && \
     gzip -f "$FILEBASE.dvi"
     RC=$?
     ;;
   ps)
+    check_root && \
     run_latex && \
     run_dvips &&
     RC=$?
     ;;
   ps.gz)
+    check_root && \
     run_latex && \
     run_dvips &&
     gzip -f "$FILEBASE.ps"
     RC=$?
     ;;
   pdf)
+    check_root && \
     run_pdflatex
     RC=$?
     ;;
   bbl)
+    check_root && \
     run_bibtex
     RC=$?
     ;;
   png)
+    check_root && \
     run_thumbpdf
     RC=$?
     ;;
+  sty)
+    update_styles
+    RC=$?
+    ;;
   *)
     fail "Bad output format '$OUTFORMAT'"
     ;;