# HG changeset patch
# User wenzelm
# Date 1621418098 -7200
# Node ID c46ff0efa1cef6b62c53edfc12fec57af7447dcf
# Parent  3e44f8c3f0599cddfc3bbe207a3c2fcaa3b5a5d1
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
clarified ISABELLE_MAKEINDEX options;

diff -r 3e44f8c3f059 -r c46ff0efa1ce etc/settings
--- a/etc/settings	Wed May 19 11:48:35 2021 +0200
+++ b/etc/settings	Wed May 19 11:54:58 2021 +0200
@@ -72,7 +72,7 @@
 
 ISABELLE_LUALATEX="lualatex --interaction=nonstopmode --file-line-error"
 ISABELLE_BIBTEX="bibtex"
-ISABELLE_MAKEINDEX="makeindex"
+ISABELLE_MAKEINDEX="makeindex -c -q"
 ISABELLE_EPSTOPDF="epstopdf"
 
 
diff -r 3e44f8c3f059 -r c46ff0efa1ce src/Doc/Tutorial/document/build
--- a/src/Doc/Tutorial/document/build	Wed May 19 11:48:35 2021 +0200
+++ b/src/Doc/Tutorial/document/build	Wed May 19 11:54:58 2021 +0200
@@ -2,12 +2,9 @@
 
 set -e
 
-FORMAT="$1"
-VARIANT="$2"
-
-isabelle latex -o "$FORMAT"
-isabelle latex -o bbl
-isabelle latex -o "$FORMAT"
-isabelle latex -o "$FORMAT"
+$ISABELLE_LUALATEX root
+$ISABELLE_BIBTEX root
+$ISABELLE_LUALATEX root
+$ISABELLE_LUALATEX root
 ./isa-index root
-isabelle latex -o "$FORMAT"
+$ISABELLE_LUALATEX root
diff -r 3e44f8c3f059 -r c46ff0efa1ce src/Doc/Tutorial/document/isa-index
--- a/src/Doc/Tutorial/document/isa-index	Wed May 19 11:48:35 2021 +0200
+++ b/src/Doc/Tutorial/document/isa-index	Wed May 19 11:54:58 2021 +0200
@@ -20,4 +20,4 @@
 s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
 s~\*\(\".\".\)~\1@\\\\isa {\1}~g
 s~\*\(\".\)~\1@\\\\isa {\1}~g
-s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind
+s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | $ISABELLE_MAKEINDEX -o $1.ind
diff -r 3e44f8c3f059 -r c46ff0efa1ce src/Doc/prepare_document
--- a/src/Doc/prepare_document	Wed May 19 11:48:35 2021 +0200
+++ b/src/Doc/prepare_document	Wed May 19 11:54:58 2021 +0200
@@ -2,20 +2,18 @@
 
 set -e
 
-FORMAT="$1"
-
-isabelle latex -o "$FORMAT"
+$ISABELLE_LUALATEX root
 
 if [ -f root.bib ]
 then
-  isabelle latex -o bbl
-  isabelle latex -o "$FORMAT"
+  $ISABELLE_BIBTEX root
+  $ISABELLE_LUALATEX root
 fi
 
-isabelle latex -o "$FORMAT"
+$ISABELLE_LUALATEX root
 
 if [ -f root.idx ]
 then
   "$ISABELLE_HOME/src/Doc/sedindex" root
-  isabelle latex -o "$FORMAT"
+  $ISABELLE_LUALATEX root
 fi
diff -r 3e44f8c3f059 -r c46ff0efa1ce src/Doc/sedindex
--- a/src/Doc/sedindex	Wed May 19 11:48:35 2021 +0200
+++ b/src/Doc/sedindex	Wed May 19 11:54:58 2021 +0200
@@ -18,4 +18,4 @@
 s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g
 s~\*\(\".\".\)~\1@{\\\\tt \1}~g
 s~\*\(\".\)~\1@{\\\\tt \1}~g
-s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | makeindex -c -q -o $1.ind
+s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | $ISABELLE_MAKEINDEX -o $1.ind