diff -r 821ce370b7fc -r eec610972763 lib/Tools/latex
--- a/lib/Tools/latex	Sat Jul 27 22:16:04 2013 +0200
+++ b/lib/Tools/latex	Sat Jul 27 22:20:25 2013 +0200
@@ -13,8 +13,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
   echo
   echo "  Options are:"
-  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
-  echo "                 pdf, bbl, idx, sty, syms"
+  echo "    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty, syms"
   echo
   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
   echo "  producing the specified output format."
@@ -33,7 +32,7 @@
 
 # options
 
-OUTFORMAT=dvi
+OUTFORMAT=pdf
 
 while getopts "o:" OPT
 do
@@ -75,7 +74,6 @@
 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
-function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
 function copy_styles ()
 {
   for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
@@ -96,35 +94,16 @@
 }
 
 case "$OUTFORMAT" in
+  pdf)
+    check_root && \
+    run_pdflatex
+    RC="$?"
+    ;;
   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