Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
authorwenzelm
Wed, 19 May 2021 11:54:58 +0200
changeset 73740 c46ff0efa1ce
parent 73739 3e44f8c3f059
child 73741 941915a3b811
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;
etc/settings file | annotate | diff | comparison | revisions
src/Doc/Tutorial/document/build file | annotate | diff | comparison | revisions
src/Doc/Tutorial/document/isa-index file | annotate | diff | comparison | revisions
src/Doc/prepare_document file | annotate | diff | comparison | revisions
src/Doc/sedindex file | annotate | diff | comparison | revisions 
--- 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"
 
 
--- 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
--- 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
--- 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
--- 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
isabelle