--- a/NEWS Wed May 19 11:54:58 2021 +0200
+++ b/NEWS Wed May 19 13:00:42 2021 +0200
@@ -39,30 +39,43 @@
specifies the name of the logo variant, while "_" (underscore) refers to
the unnamed variant. The output file name is always "isabelle_logo.pdf".
+* Option "document_preprocessor" specifies the name of an executable
+that is run within the document output directory, after preparing the
+document sources and before the actual build process. This allows to
+apply adhoc patches, without requiring a separate "build" script.
+
* Option "document_build" determines the document build engine, as
defined in Isabelle/Scala (as system service). The subsequent engines
are provided by the Isabelle distribution:
- . "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX
+ - "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX
build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX
- . "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for
+ - "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for
special LaTeX styles)
- . "build": delegate to the executable "./build pdf"
+ - "build": delegate to the executable "./build pdf"
The presence of a "build" command within the document output directory
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
adjust session ROOT options.
-* Option "document_preprocessor" specifies the name of an executable
-that is run within the document output directory, after preparing the
-document sources and before the actual build process. This allows to
-apply adhoc patches, without requiring a separate "build" script.
-
-* Isabelle .sty files are automatically generated within the document
-output directory; former "isabelle latex -o sty" has been discontinued.
-Minor INCOMPATIBILITY in document build scripts.
+* The command-line tool "isabelle latex" has been discontinued,
+INCOMPATIBILITY for old document build scripts.
+
+ - Former "isabelle latex -o sty" has become obsolete: Isabelle .sty
+ files are automatically generated within the document output
+ directory.
+
+ - Former "isabelle latex -o pdf" should be replaced by
+ "$ISABELLE_LUALATEX root" or "$ISABELLE_PDFLATEX root" (without
+ quotes), according to the intended LaTeX engine.
+
+ - Former "isabelle latex -o bbl" should be replaced by
+ "$ISABELLE_BIBTEX root" (without quotes).
+
+ - Former "isabelle latex -o idx" should be replaced by
+ "$ISABELLE_MAKEINDEX root" (without quotes).
* Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
--- a/lib/Tools/latex Wed May 19 11:54:58 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: run LaTeX (and related tools)
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
- echo
- echo " Options are:"
- echo " -o FORMAT specify output format: pdf (default), bbl, idx"
- echo
- echo " Run LaTeX (and related tools) on FILE (default root.tex),"
- echo " producing the specified output format."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-OUTFORMAT=pdf
-
-while getopts "o:" OPT
-do
- case "$OPT" in
- o)
- OUTFORMAT="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-FILE="root.tex"
-[ "$#" -ge 1 ] && { FILE="$1"; shift; }
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-# root file
-
-DIR="$(dirname "$FILE")"
-FILEBASE="$(basename "$FILE" .tex)"
-[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
-
-function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
-
-
-# operations
-
-case "$OUTFORMAT" in
- pdf)
- check_root
- $ISABELLE_PDFLATEX "$FILEBASE.tex"
- RC="$?"
- ;;
- bbl)
- check_root
- $ISABELLE_BIBTEX </dev/null "$FILEBASE"
- RC="$?"
- ;;
- idx)
- check_root
- $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"
- RC="$?"
- ;;
- *)
- fail "Bad output format '$OUTFORMAT'"
- ;;
-esac
-
-exit "$RC"
--- a/src/Doc/JEdit/JEdit.thy Wed May 19 11:54:58 2021 +0200
+++ b/src/Doc/JEdit/JEdit.thy Wed May 19 13:00:42 2021 +0200
@@ -1911,7 +1911,7 @@
text \<open>
Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The
- Isabelle session build process and the @{tool latex} tool @{cite
+ Isabelle session build process and the @{tool document} tool @{cite
"isabelle-system"} are smart enough to assemble the result, based on the
session directory layout.
--- a/src/Doc/System/Environment.thy Wed May 19 11:54:58 2021 +0200
+++ b/src/Doc/System/Environment.thy Wed May 19 13:00:42 2021 +0200
@@ -181,9 +181,10 @@
\<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
@{tool_ref console} interface.
- \<^descr>[@{setting_def ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to
- {\LaTeX} related tools for Isabelle document preparation (see also
- \secref{sec:tool-latex}).
+ \<^descr>[@{setting_def ISABELLE_PDFLATEX}, @{setting_def ISABELLE_LUALATEX},
+ @{setting_def ISABELLE_BIBTEX}, @{setting_def ISABELLE_MAKEINDEX}] refer to
+ {\LaTeX}-related tools for Isabelle document preparation (see also
+ \secref{sec:tool-document}).
\<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
that are scanned by @{executable isabelle} for external utility programs
--- a/src/Doc/System/Presentation.thy Wed May 19 11:54:58 2021 +0200
+++ b/src/Doc/System/Presentation.thy Wed May 19 13:00:42 2021 +0200
@@ -22,8 +22,7 @@
with the PDF into the given directory (relative to the session directory).
Alternatively, @{tool_ref document} may be used to turn the generated
- {\LaTeX} sources of a session (exports from its build database) into PDF,
- using suitable invocations of @{tool_ref latex}.
+ {\LaTeX} sources of a session (exports from its build database) into PDF.
\<close>
@@ -161,12 +160,20 @@
\<^medskip> Isabelle is usually smart enough to create the PDF from the given
\<^verbatim>\<open>root.tex\<close> and optional \<^verbatim>\<open>root.bib\<close> (bibliography) and \<^verbatim>\<open>root.idx\<close> (index)
- using standard {\LaTeX} tools. Alternatively, \isakeyword{document\_files}
- in the session \<^verbatim>\<open>ROOT\<close> may include an executable \<^verbatim>\<open>build\<close> script to take
- care of that. It is invoked with command-line arguments for the document
- format (\<^verbatim>\<open>pdf\<close>) and the document variant name. The script needs to produce
- corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for default document variants
- (the main work can be delegated to @{tool latex}). \<close>
+ using standard {\LaTeX} tools. Actual command-lines are given by settings
+ @{setting_ref ISABELLE_PDFLATEX}, @{setting_ref ISABELLE_LUALATEX},
+ @{setting_ref ISABELLE_BIBTEX}, @{setting_ref ISABELLE_MAKEINDEX}: these
+ variables are used without quoting in shell scripts, and thus may contain
+ additional options.
+
+ Alternatively, the session \<^verbatim>\<open>ROOT\<close> may include an option
+ \<^verbatim>\<open>document_build=build\<close> together with an executable \<^verbatim>\<open>build\<close> script in
+ \isakeyword{document\_files}: it is invoked with command-line arguments for
+ the document format (\<^verbatim>\<open>pdf\<close>) and the document variant name. The script needs
+ to produce corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for default
+ document variants.
+\<close>
+
subsubsection \<open>Examples\<close>
@@ -177,43 +184,4 @@
@{verbatim [display] \<open>isabelle document -v -V -O. FOL\<close>}
\<close>
-
-section \<open>Running {\LaTeX} within the Isabelle environment
- \label{sec:tool-latex}\<close>
-
-text \<open>
- The @{tool_def latex} tool provides the basic interface for Isabelle
- document preparation. Its usage is:
- @{verbatim [display]
-\<open>Usage: isabelle latex [OPTIONS] [FILE]
-
- Options are:
- -o FORMAT specify output format: pdf (default), bbl, idx
-
- Run LaTeX (and related tools) on FILE (default root.tex),
- producing the specified output format.\<close>}
-
- Appropriate {\LaTeX}-related programs are run on the input file, according
- to the given output format: @{executable pdflatex}, @{executable bibtex}
- (for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands
- are determined from the settings environment (@{setting ISABELLE_PDFLATEX}
- etc.).
-\<close>
-
-
-subsubsection \<open>Examples\<close>
-
-text \<open>
- Invoking @{tool latex} by hand may be occasionally useful when debugging
- failed attempts of the automatic document preparation stage of batch-mode
- Isabelle. The abortive process leaves the sources at a certain place within
- @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.
- This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like
- this:
-
- @{verbatim [display]
-\<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
-isabelle latex -o pdf\<close>}
-\<close>
-
end