# HG changeset patch # User wenzelm # Date 1621422042 -7200 # Node ID 941915a3b811affb17439bd9342295abf32d332a # Parent c46ff0efa1cef6b62c53edfc12fec57af7447dcf discontinued obsolete "isabelle latex"; diff -r c46ff0efa1ce -r 941915a3b811 NEWS --- 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 \...\ using \guilsinglleft ... \guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc} diff -r c46ff0efa1ce -r 941915a3b811 lib/Tools/latex --- 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 Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\.bib\ 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. diff -r c46ff0efa1ce -r 941915a3b811 src/Doc/System/Environment.thy --- 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 diff -r c46ff0efa1ce -r 941915a3b811 src/Doc/System/Presentation.thy --- 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. \ @@ -161,12 +160,20 @@ \<^medskip> Isabelle is usually smart enough to create the PDF from the given \<^verbatim>\root.tex\ and optional \<^verbatim>\root.bib\ (bibliography) and \<^verbatim>\root.idx\ (index) - using standard {\LaTeX} tools. Alternatively, \isakeyword{document\_files} - in the session \<^verbatim>\ROOT\ may include an executable \<^verbatim>\build\ script to take - care of that. It is invoked with command-line arguments for the document - format (\<^verbatim>\pdf\) and the document variant name. The script needs to produce - corresponding output files, e.g.\ \<^verbatim>\root.pdf\ for default document variants - (the main work can be delegated to @{tool latex}). \ + 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>\ROOT\ may include an option + \<^verbatim>\document_build=build\ together with an executable \<^verbatim>\build\ script in + \isakeyword{document\_files}: it is invoked with command-line arguments for + the document format (\<^verbatim>\pdf\) and the document variant name. The script needs + to produce corresponding output files, e.g.\ \<^verbatim>\root.pdf\ for default + document variants. +\ + subsubsection \Examples\ @@ -177,43 +184,4 @@ @{verbatim [display] \isabelle document -v -V -O. FOL\} \ - -section \Running {\LaTeX} within the Isabelle environment - \label{sec:tool-latex}\ - -text \ - The @{tool_def latex} tool provides the basic interface for Isabelle - document preparation. Its usage is: - @{verbatim [display] -\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.\} - - Appropriate {\LaTeX}-related programs are run on the input file, according - to the given output format: @{executable pdflatex}, @{executable bibtex} - (for \<^verbatim>\bbl\), and @{executable makeindex} (for \<^verbatim>\idx\). The actual commands - are determined from the settings environment (@{setting ISABELLE_PDFLATEX} - etc.). -\ - - -subsubsection \Examples\ - -text \ - 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] -\cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document" -isabelle latex -o pdf\} -\ - end