# HG changeset patch
# User wenzelm
# Date 1374956425 -7200
# Node ID eec610972763f3bb454d5183bdc9c7f944d92542
# Parent  821ce370b7fc16e151dd50cd3f8501d15fe6bdd5
discontinued historic document formats;

diff -r 821ce370b7fc -r eec610972763 NEWS
--- a/NEWS	Sat Jul 27 22:16:04 2013 +0200
+++ b/NEWS	Sat Jul 27 22:20:25 2013 +0200
@@ -323,8 +323,9 @@
 * Discontinued obsolete isabelle print tool, and PRINT_COMMAND
 settings variable.
 
-* Discontinued ISABELLE_DOC_FORMAT settings variable -- the preferred
-document format is always pdf.
+* Discontinued ISABELLE_DOC_FORMAT settings variable and historic
+document formats: dvi.gz, ps, ps.gz -- the default document format is
+always pdf.
 
 * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
 specify global resources of the JVM process run by isabelle build.
diff -r 821ce370b7fc -r eec610972763 etc/options
--- a/etc/options	Sat Jul 27 22:16:04 2013 +0200
+++ b/etc/options	Sat Jul 27 22:20:25 2013 +0200
@@ -6,7 +6,7 @@
   -- "generate theory browser information"
 
 option document : string = ""
-  -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
+  -- "build document in given format: pdf, dvi, false"
 option document_output : string = ""
   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
 option document_variants : string = "document"
diff -r 821ce370b7fc -r eec610972763 etc/settings
--- a/etc/settings	Sat Jul 27 22:16:04 2013 +0200
+++ b/etc/settings	Sat Jul 27 22:20:25 2013 +0200
@@ -39,7 +39,6 @@
 ISABELLE_PDFLATEX="pdflatex"
 ISABELLE_BIBTEX="bibtex"
 ISABELLE_MAKEINDEX="makeindex"
-ISABELLE_DVIPS="dvips -D 600"
 ISABELLE_EPSTOPDF="epstopdf"
 
 # Paranoia setting for strange latex installations ...
diff -r 821ce370b7fc -r eec610972763 lib/Tools/document
--- a/lib/Tools/document	Sat Jul 27 22:16:04 2013 +0200
+++ b/lib/Tools/document	Sat Jul 27 22:20:25 2013 +0200
@@ -15,7 +15,7 @@
   echo "  Options are:"
   echo "    -c           cleanup -- be aggressive in removing old stuff"
   echo "    -n NAME      specify document name (default 'document')"
-  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
+  echo "    -o FORMAT    specify output format: pdf (default), dvi"
   echo "    -t TAGS      specify tagged region markup"
   echo
   echo "  Prepare the theory session document in DIR (default 'document')"
@@ -37,7 +37,7 @@
 
 CLEAN=""
 NAME="document"
-OUTFORMAT=dvi
+OUTFORMAT=pdf
 declare -a TAGS=()
 
 while getopts "cn:o:t:" OPT
@@ -77,7 +77,7 @@
 # check format
 
 case "$OUTFORMAT" in
-  dvi | dvi.gz | ps | ps.gz | pdf)
+  pdf | dvi)
     ;;
   *)
     fail "Bad output format '$OUTFORMAT'"
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
diff -r 821ce370b7fc -r eec610972763 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Sat Jul 27 22:16:04 2013 +0200
+++ b/src/Doc/System/Basics.thy	Sat Jul 27 22:20:25 2013 +0200
@@ -257,9 +257,9 @@
   line editor for the @{tool_ref tty} interface.
 
   \item[@{setting_def ISABELLE_LATEX}, @{setting_def
-  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
-  ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
-  document preparation (see also \secref{sec:tool-latex}).
+  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX}
+  related tools for Isabelle document preparation (see also
+  \secref{sec:tool-latex}).
   
   \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
   directories that are scanned by @{executable isabelle} for external
diff -r 821ce370b7fc -r eec610972763 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Sat Jul 27 22:16:04 2013 +0200
+++ b/src/Doc/System/Presentation.thy	Sat Jul 27 22:20:25 2013 +0200
@@ -168,8 +168,7 @@
   Options are:
     -c           cleanup -- be aggressive in removing old stuff
     -n NAME      specify document name (default 'document')
-    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
-                 ps.gz, pdf
+    -o FORMAT    specify output format: pdf (default), dvi
     -t TAGS      specify tagged region markup
 
   Prepare the theory session document in DIR (default 'document')
@@ -276,8 +275,8 @@
 Usage: isabelle latex [OPTIONS] [FILE]
 
   Options are:
-    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
-                 ps.gz, pdf, bbl, idx, sty, syms
+    -o FORMAT    specify output format: pdf (default), dvi,
+                 bbl, idx, sty, syms
 
   Run LaTeX (and related tools) on FILE (default root.tex),
   producing the specified output format.