discontinued obsolete "isabelle latex";
authorwenzelm
Wed, 19 May 2021 13:00:42 +0200
changeset 73997 941915a3b811
parent 73996 c46ff0efa1ce
child 73998 c31510e70e95
discontinued obsolete "isabelle latex";
NEWS
lib/Tools/latex
src/Doc/JEdit/JEdit.thy
src/Doc/System/Environment.thy
src/Doc/System/Presentation.thy
--- 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