--- a/NEWS Mon Sep 28 18:34:15 2020 +0100
+++ b/NEWS Mon Sep 28 18:34:27 2020 +0100
@@ -32,15 +32,20 @@
*** Document preparation ***
+* The standard LaTeX engine is now lualatex, according to settings
+variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
+pdflatex, but text encoding needs to conform strictly to utf8. Rare
+INCOMPATIBILITY.
+
+* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
+document output is always PDF.
+
* Antiquotation @{bash_function} refers to GNU bash functions that are
checked within the Isabelle settings environment.
* Antiquotations @{scala}, @{scala_object}, @{scala_type},
@{scala_method} refer to checked Isabelle/Scala entities.
-* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
-document output is always PDF.
-
*** Pure ***
@@ -164,6 +169,10 @@
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
variable.
+* The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
+(for DVI documents) has been discontinued. Former option -n has been
+turned into -o with explicit file name. Minor INCOMPATIBILITY.
+
* The shell function "isabelle_directory" (within etc/settings of
components) augments the list of special directories for persistent
symbolic path names. This improves portability of heap images and
--- a/etc/settings Mon Sep 28 18:34:15 2020 +0100
+++ b/etc/settings Mon Sep 28 18:34:27 2020 +0100
@@ -59,15 +59,11 @@
### Document preparation (cf. isabelle latex/document)
###
-ISABELLE_PDFLATEX="pdflatex -file-line-error"
+ISABELLE_PDFLATEX="lualatex --file-line-error"
ISABELLE_BIBTEX="bibtex"
ISABELLE_MAKEINDEX="makeindex"
ISABELLE_EPSTOPDF="epstopdf"
-if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
- ISABELLE_PDFLATEX="pdflatex -c-style-errors"
-fi
-
###
### Misc path settings
--- a/lib/Tools/logo Mon Sep 28 18:34:15 2020 +0100
+++ b/lib/Tools/logo Mon Sep 28 18:34:27 2020 +0100
@@ -1,8 +1,8 @@
#!/usr/bin/env bash
#
-# Author: Markus Wenzel, TU Muenchen
+# Author: Makarius
#
-# DESCRIPTION: create an instance of the Isabelle logo
+# DESCRIPTION: create an instance of the Isabelle logo (PDF)
PRG="$(basename "$0")"
@@ -12,10 +12,10 @@
echo
echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
echo
- echo " Create instance XYZ of the Isabelle logo (as EPS and PDF)."
+ echo " Create instance XYZ of the Isabelle logo (PDF)."
echo
echo " Options are:"
- echo " -n NAME alternative output base name (default \"isabelle_xyx\")"
+ echo " -o FILE alternative output file (default \"isabelle_xyx.pdf\")"
echo " -q quiet mode"
echo
exit 1
@@ -32,14 +32,14 @@
# options
-OUTPUT_NAME=""
+OUTPUT_FILE=""
QUIET=""
-while getopts "n:q" OPT
+while getopts "o:q" OPT
do
case "$OPT" in
- n)
- OUTPUT_NAME="$OPTARG"
+ o)
+ OUTPUT_FILE="$OPTARG"
;;
q)
QUIET=true
@@ -63,25 +63,15 @@
## main
-case "$OUTPUT_NAME" in
- "")
- OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z)
- if [ -z "$OUTPUT_NAME" ]; then
- OUTPUT_NAME="isabelle"
- else
- OUTPUT_NAME="isabelle_${OUTPUT_NAME}"
- fi
- ;;
- */* | *.eps | *.pdf)
- fail "Bad output base name: \"$OUTPUT_NAME\""
- ;;
- *)
- ;;
-esac
+if [ -z "$OUTPUT_FILE" ]; then
+ OUTPUT_NAME="$(echo "$TEXT" | tr A-Z a-z)"
+ if [ -z "$OUTPUT_NAME" ]; then
+ OUTPUT_FILE="isabelle.pdf"
+ else
+ OUTPUT_FILE="isabelle_${OUTPUT_NAME}.pdf"
+ fi
+fi
-[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
-perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
-
-[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
-"$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"
-
+[ -z "$QUIET" ] && echo "$OUTPUT_FILE" >&2
+perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
+ "$ISABELLE_EPSTOPDF" --filter > "$OUTPUT_FILE"
--- a/src/Doc/Prog_Prove/Logic.thy Mon Sep 28 18:34:15 2020 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy Mon Sep 28 18:34:27 2020 +0100
@@ -49,7 +49,7 @@
\<open>\<forall>\<close> & \xsymbol{forall} & \texttt{ALL}\\
\<open>\<exists>\<close> & \xsymbol{exists} & \texttt{EX}\\
\<open>\<lambda>\<close> & \xsymbol{lambda} & \texttt{\%}\\
-\<open>\<longrightarrow>\<close> & \texttt{-{}->}\\
+\<open>\<longrightarrow>\<close> & \texttt{-{\kern0pt}->}\\
\<open>\<longleftrightarrow>\<close> & \texttt{<->}\\
\<open>\<and>\<close> & \texttt{/\char`\\} & \texttt{\&}\\
\<open>\<or>\<close> & \texttt{\char`\\/} & \texttt{|}\\
--- a/src/Doc/Sledgehammer/document/build Mon Sep 28 18:34:15 2020 +0100
+++ b/src/Doc/Sledgehammer/document/build Mon Sep 28 18:34:27 2020 +0100
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo -n isabelle_sledgehammer "S/H"
+isabelle logo -o isabelle_sledgehammer.pdf "S/H"
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
-
--- a/src/Doc/System/Misc.thy Mon Sep 28 18:34:15 2020 +0100
+++ b/src/Doc/System/Misc.thy Mon Sep 28 18:34:27 2020 +0100
@@ -321,21 +321,21 @@
section \<open>Creating instances of the Isabelle logo\<close>
text \<open>
- The @{tool_def logo} tool creates instances of the generic Isabelle logo as
- EPS and PDF, for inclusion in {\LaTeX} documents.
+ The @{tool_def logo} tool creates instances of the generic Isabelle logo,
+ for inclusion in PDF{\LaTeX} documents.
@{verbatim [display]
-\<open>Usage: isabelle logo [OPTIONS] XYZ
+\<open>Usage: isabelle logo [OPTIONS] [XYZ]
- Create instance XYZ of the Isabelle logo (as EPS and PDF).
+ Create instance XYZ of the Isabelle logo (PDF).
Options are:
- -n NAME alternative output base name (default "isabelle_xyx")
+ -o FILE alternative output file (default "isabelle_xyx.pdf")
-q quiet mode\<close>}
- Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the generated files.
- The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close> in lower-case.
+ Option \<^verbatim>\<open>-o\<close> specifies an alternative output file: the default is
+ \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close>\<^verbatim>\<open>.pdf\<close> (in lower-case).
- Option \<^verbatim>\<open>-q\<close> omits printing of the result file name.
+ Option \<^verbatim>\<open>-q\<close> omits printing of the resulting output file name.
\<^medskip>
Implementors of Isabelle tools and applications are encouraged to make
--- a/src/HOL/Analysis/Gamma_Function.thy Mon Sep 28 18:34:15 2020 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Mon Sep 28 18:34:27 2020 +0100
@@ -18,7 +18,7 @@
most important properties. Also contains the definition and some properties
of the log-Gamma function and the Digamma function and the other Polygamma functions.
- Based on the Gamma function, we also prove the Weierstraß product form of the
+ Based on the Gamma function, we also prove the Weierstra{\ss} product form of the
sin function and, based on this, the solution of the Basel problem (the
sum over all \<^term>\<open>1 / (n::nat)^2\<close>.
\<close>
@@ -3349,7 +3349,7 @@
qed
-subsection \<open>The Weierstraß product formula for the sine\<close>
+subsection \<open>The Weierstra{\ss} product formula for the sine\<close>
theorem sin_product_formula_complex:
fixes z :: complex
--- a/src/HOL/Library/Tree.thy Mon Sep 28 18:34:15 2020 +0100
+++ b/src/HOL/Library/Tree.thy Mon Sep 28 18:34:27 2020 +0100
@@ -153,6 +153,9 @@
lemma neq_empty_subtrees[simp]: "{} \<noteq> subtrees t"
by (cases t)(auto)
+lemma size_subtrees: "s \<in> subtrees t \<Longrightarrow> size s \<le> size t"
+by(induction t)(auto)
+
lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t"
by (induction t)(auto)
--- a/src/HOL/ROOT Mon Sep 28 18:34:15 2020 +0100
+++ b/src/HOL/ROOT Mon Sep 28 18:34:27 2020 +0100
@@ -318,8 +318,9 @@
theories Hoare_Parallel
document_files "root.bib" "root.tex"
-session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
+session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
sessions
+ "HOL-Number_Theory"
"HOL-Data_Structures"
"HOL-Examples"
"HOL-Word"
--- a/src/Pure/Admin/isabelle_cronjob.scala Mon Sep 28 18:34:15 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Sep 28 18:34:27 2020 +0100
@@ -328,7 +328,9 @@
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
- detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
+ detect =
+ Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows") + " OR " +
+ Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")),
Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
options = "-m64 -M4" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
--- a/src/Pure/PIDE/protocol.ML Mon Sep 28 18:34:15 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML Mon Sep 28 18:34:27 2020 +0100
@@ -182,4 +182,3 @@
(fn [] => ML_Heap.share_common_data ());
end;
-
--- a/src/Pure/Thy/latex.ML Mon Sep 28 18:34:15 2020 +0100
+++ b/src/Pure/Thy/latex.ML Mon Sep 28 18:34:27 2020 +0100
@@ -115,8 +115,9 @@
| "\t" => "\\ "
| "\n" => "\\isanewline\n"
| s =>
- if exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~"
- then enclose "{\\char`\\" "}" s else s);
+ s
+ |> exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" ? enclose "{\\char`\\" "}"
+ |> suffix "{\\kern0pt}");
fun output_ascii_breakable sep =
space_explode sep
@@ -169,7 +170,7 @@
| output_chr "\n" = "\\isanewline\n"
| output_chr c =
(case Symtab.lookup char_table c of
- SOME s => s
+ SOME s => s ^ "{\\kern0pt}"
| NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
fun output_sym sym =
--- a/src/Pure/Thy/present.ML Mon Sep 28 18:34:15 2020 +0100
+++ b/src/Pure/Thy/present.ML Mon Sep 28 18:34:27 2020 +0100
@@ -6,6 +6,7 @@
signature PRESENT =
sig
+ val tex_path: string -> Path.T
val get_bibtex_entries: theory -> string list
val theory_qualifier: theory -> string
val document_option: Options.T -> {enabled: bool, disabled: bool}
@@ -31,7 +32,7 @@
val readme_html_path = Path.basic "README.html";
val doc_indexN = "session";
val session_graph_path = Path.basic "session_graph.pdf";
-fun document_path name = Path.basic name |> Path.ext "pdf";
+val document_path = Path.ext "pdf" o Path.basic;
fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));
--- a/src/Pure/Thy/thy_info.ML Mon Sep 28 18:34:15 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Sep 28 18:34:27 2020 +0100
@@ -66,9 +66,12 @@
if #disabled option then ()
else
let
- val latex = Latex.isabelle_body (Context.theory_name thy) body;
+ val thy_name = Context.theory_name thy;
+ val document_path = Path.append (Path.basic "document") (Present.tex_path thy_name);
+
+ val latex = Latex.isabelle_body thy_name body;
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
- val _ = Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output);
+ val _ = Export.export thy (Path.binding0 document_path) (XML.blob output);
val _ = if #enabled option then Present.theory_output thy output else ();
in () end
end));