discontinued historic document formats;
authorwenzelm
Sat Jul 27 22:20:25 2013 +0200 (2013-07-27)
changeset 52746eec610972763
parent 52745 821ce370b7fc
child 52747 2130b5c4b287
discontinued historic document formats;
NEWS
etc/options
etc/settings
lib/Tools/document
lib/Tools/latex
src/Doc/System/Basics.thy
src/Doc/System/Presentation.thy
     1.1 --- a/NEWS	Sat Jul 27 22:16:04 2013 +0200
     1.2 +++ b/NEWS	Sat Jul 27 22:20:25 2013 +0200
     1.3 @@ -323,8 +323,9 @@
     1.4  * Discontinued obsolete isabelle print tool, and PRINT_COMMAND
     1.5  settings variable.
     1.6  
     1.7 -* Discontinued ISABELLE_DOC_FORMAT settings variable -- the preferred
     1.8 -document format is always pdf.
     1.9 +* Discontinued ISABELLE_DOC_FORMAT settings variable and historic
    1.10 +document formats: dvi.gz, ps, ps.gz -- the default document format is
    1.11 +always pdf.
    1.12  
    1.13  * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
    1.14  specify global resources of the JVM process run by isabelle build.
     2.1 --- a/etc/options	Sat Jul 27 22:16:04 2013 +0200
     2.2 +++ b/etc/options	Sat Jul 27 22:20:25 2013 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4    -- "generate theory browser information"
     2.5  
     2.6  option document : string = ""
     2.7 -  -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
     2.8 +  -- "build document in given format: pdf, dvi, false"
     2.9  option document_output : string = ""
    2.10    -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
    2.11  option document_variants : string = "document"
     3.1 --- a/etc/settings	Sat Jul 27 22:16:04 2013 +0200
     3.2 +++ b/etc/settings	Sat Jul 27 22:20:25 2013 +0200
     3.3 @@ -39,7 +39,6 @@
     3.4  ISABELLE_PDFLATEX="pdflatex"
     3.5  ISABELLE_BIBTEX="bibtex"
     3.6  ISABELLE_MAKEINDEX="makeindex"
     3.7 -ISABELLE_DVIPS="dvips -D 600"
     3.8  ISABELLE_EPSTOPDF="epstopdf"
     3.9  
    3.10  # Paranoia setting for strange latex installations ...
     4.1 --- a/lib/Tools/document	Sat Jul 27 22:16:04 2013 +0200
     4.2 +++ b/lib/Tools/document	Sat Jul 27 22:20:25 2013 +0200
     4.3 @@ -15,7 +15,7 @@
     4.4    echo "  Options are:"
     4.5    echo "    -c           cleanup -- be aggressive in removing old stuff"
     4.6    echo "    -n NAME      specify document name (default 'document')"
     4.7 -  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
     4.8 +  echo "    -o FORMAT    specify output format: pdf (default), dvi"
     4.9    echo "    -t TAGS      specify tagged region markup"
    4.10    echo
    4.11    echo "  Prepare the theory session document in DIR (default 'document')"
    4.12 @@ -37,7 +37,7 @@
    4.13  
    4.14  CLEAN=""
    4.15  NAME="document"
    4.16 -OUTFORMAT=dvi
    4.17 +OUTFORMAT=pdf
    4.18  declare -a TAGS=()
    4.19  
    4.20  while getopts "cn:o:t:" OPT
    4.21 @@ -77,7 +77,7 @@
    4.22  # check format
    4.23  
    4.24  case "$OUTFORMAT" in
    4.25 -  dvi | dvi.gz | ps | ps.gz | pdf)
    4.26 +  pdf | dvi)
    4.27      ;;
    4.28    *)
    4.29      fail "Bad output format '$OUTFORMAT'"
     5.1 --- a/lib/Tools/latex	Sat Jul 27 22:16:04 2013 +0200
     5.2 +++ b/lib/Tools/latex	Sat Jul 27 22:20:25 2013 +0200
     5.3 @@ -13,8 +13,7 @@
     5.4    echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
     5.5    echo
     5.6    echo "  Options are:"
     5.7 -  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
     5.8 -  echo "                 pdf, bbl, idx, sty, syms"
     5.9 +  echo "    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty, syms"
    5.10    echo
    5.11    echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    5.12    echo "  producing the specified output format."
    5.13 @@ -33,7 +32,7 @@
    5.14  
    5.15  # options
    5.16  
    5.17 -OUTFORMAT=dvi
    5.18 +OUTFORMAT=pdf
    5.19  
    5.20  while getopts "o:" OPT
    5.21  do
    5.22 @@ -75,7 +74,6 @@
    5.23  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    5.24  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    5.25  function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
    5.26 -function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    5.27  function copy_styles ()
    5.28  {
    5.29    for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
    5.30 @@ -96,35 +94,16 @@
    5.31  }
    5.32  
    5.33  case "$OUTFORMAT" in
    5.34 +  pdf)
    5.35 +    check_root && \
    5.36 +    run_pdflatex
    5.37 +    RC="$?"
    5.38 +    ;;
    5.39    dvi)
    5.40      check_root && \
    5.41      run_latex
    5.42      RC="$?"
    5.43      ;;
    5.44 -  dvi.gz)
    5.45 -    check_root && \
    5.46 -    run_latex && \
    5.47 -    gzip -f "$FILEBASE.dvi"
    5.48 -    RC="$?"
    5.49 -    ;;
    5.50 -  ps)
    5.51 -    check_root && \
    5.52 -    run_latex && \
    5.53 -    run_dvips
    5.54 -    RC="$?"
    5.55 -    ;;
    5.56 -  ps.gz)
    5.57 -    check_root && \
    5.58 -    run_latex && \
    5.59 -    run_dvips && \
    5.60 -    gzip -f "$FILEBASE.ps"
    5.61 -    RC="$?"
    5.62 -    ;;
    5.63 -  pdf)
    5.64 -    check_root && \
    5.65 -    run_pdflatex
    5.66 -    RC="$?"
    5.67 -    ;;
    5.68    bbl)
    5.69      check_root && \
    5.70      run_bibtex
     6.1 --- a/src/Doc/System/Basics.thy	Sat Jul 27 22:16:04 2013 +0200
     6.2 +++ b/src/Doc/System/Basics.thy	Sat Jul 27 22:20:25 2013 +0200
     6.3 @@ -257,9 +257,9 @@
     6.4    line editor for the @{tool_ref tty} interface.
     6.5  
     6.6    \item[@{setting_def ISABELLE_LATEX}, @{setting_def
     6.7 -  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
     6.8 -  ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
     6.9 -  document preparation (see also \secref{sec:tool-latex}).
    6.10 +  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX}
    6.11 +  related tools for Isabelle document preparation (see also
    6.12 +  \secref{sec:tool-latex}).
    6.13    
    6.14    \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
    6.15    directories that are scanned by @{executable isabelle} for external
     7.1 --- a/src/Doc/System/Presentation.thy	Sat Jul 27 22:16:04 2013 +0200
     7.2 +++ b/src/Doc/System/Presentation.thy	Sat Jul 27 22:20:25 2013 +0200
     7.3 @@ -168,8 +168,7 @@
     7.4    Options are:
     7.5      -c           cleanup -- be aggressive in removing old stuff
     7.6      -n NAME      specify document name (default 'document')
     7.7 -    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
     7.8 -                 ps.gz, pdf
     7.9 +    -o FORMAT    specify output format: pdf (default), dvi
    7.10      -t TAGS      specify tagged region markup
    7.11  
    7.12    Prepare the theory session document in DIR (default 'document')
    7.13 @@ -276,8 +275,8 @@
    7.14  Usage: isabelle latex [OPTIONS] [FILE]
    7.15  
    7.16    Options are:
    7.17 -    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
    7.18 -                 ps.gz, pdf, bbl, idx, sty, syms
    7.19 +    -o FORMAT    specify output format: pdf (default), dvi,
    7.20 +                 bbl, idx, sty, syms
    7.21  
    7.22    Run LaTeX (and related tools) on FILE (default root.tex),
    7.23    producing the specified output format.