# HG changeset patch
# User paulson
# Date 1601314467 -3600
# Node ID fb6295a224f835aa13d63a0acc6b72f44d3ee4fe
# Parent  bc97bd4c0474415e2374a55b5f84e23a781574e9# Parent  7bb074cceefed78e74708bb23c878c4cb3b75430
merged

diff -r 7bb074cceefe -r fb6295a224f8 NEWS
--- 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
diff -r 7bb074cceefe -r fb6295a224f8 etc/settings
--- 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
diff -r 7bb074cceefe -r fb6295a224f8 lib/Tools/logo
--- 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"
diff -r 7bb074cceefe -r fb6295a224f8 src/Doc/Prog_Prove/Logic.thy
--- 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{|}\\
diff -r 7bb074cceefe -r fb6295a224f8 src/Doc/Sledgehammer/document/build
--- 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"
-
diff -r 7bb074cceefe -r fb6295a224f8 src/Doc/System/Misc.thy
--- 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
diff -r 7bb074cceefe -r fb6295a224f8 src/HOL/Analysis/Gamma_Function.thy
--- 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
diff -r 7bb074cceefe -r fb6295a224f8 src/HOL/Library/Tree.thy
--- 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)
 
diff -r 7bb074cceefe -r fb6295a224f8 src/HOL/ROOT
--- 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"
diff -r 7bb074cceefe -r fb6295a224f8 src/Pure/Admin/isabelle_cronjob.scala
--- 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" +
diff -r 7bb074cceefe -r fb6295a224f8 src/Pure/PIDE/protocol.ML
--- 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;
-
diff -r 7bb074cceefe -r fb6295a224f8 src/Pure/Thy/latex.ML
--- 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 =
diff -r 7bb074cceefe -r fb6295a224f8 src/Pure/Thy/present.ML
--- 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));
 
diff -r 7bb074cceefe -r fb6295a224f8 src/Pure/Thy/thy_info.ML
--- 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));