diff --git a/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,188 +1,188 @@ # -*- shell-script -*- :mode=shellscript: # # Isabelle system settings. # # Important notes: # * See the "system" manual for explanations on Isabelle settings # * User settings go into $ISABELLE_HOME_USER/etc/settings # * DO NOT EDIT the repository copy of this file! # * DO NOT COPY this file into the $ISABELLE_HOME_USER directory! ### ### Isabelle/Scala ### ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0" ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -Wconf:cat=other-match-analysis:silent -feature -deprecation -target:11 -Xsource:3 -J-Xms512m -J-Xmx4g -J-Xss16m" classpath "$ISABELLE_HOME/lib/classes/Pure.jar" isabelle_scala_service 'isabelle.Tools' [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools' isabelle_scala_service 'isabelle.Scala_Functions' isabelle_scala_service 'isabelle.Sessions$File_Format' isabelle_scala_service 'isabelle.Bibtex$File_Format' isabelle_scala_service 'isabelle.ML_Statistics$Handler' isabelle_scala_service 'isabelle.Scala$Handler' isabelle_scala_service 'isabelle.Print_Operation$Handler' isabelle_scala_service 'isabelle.Simplifier_Trace$Handler' isabelle_scala_service 'isabelle.Server_Commands' isabelle_scala_service 'isabelle.Document_Build$LuaLaTeX_Engine' isabelle_scala_service 'isabelle.Document_Build$PDFLaTeX_Engine' isabelle_scala_service 'isabelle.Document_Build$Build_Engine' #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS ### ### Interactive sessions (cf. isabelle console) ### ISABELLE_LINE_EDITOR="rlwrap" ### ### Batch sessions (cf. isabelle build) ### ISABELLE_BUILD_OPTIONS="" ### ### Document preparation (cf. isabelle latex) ### if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -c-style-errors" else ISABELLE_PDFLATEX="pdflatex -interaction=nonstopmode -file-line-error" fi ISABELLE_LUALATEX="lualatex --interaction=nonstopmode --file-line-error" ISABELLE_BIBTEX="bibtex" -ISABELLE_MAKEINDEX="makeindex" +ISABELLE_MAKEINDEX="makeindex -c -q" ISABELLE_EPSTOPDF="epstopdf" ### ### Misc path settings ### isabelle_directory '~' isabelle_directory '$ISABELLE_HOME_USER' isabelle_directory '~~' ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components" ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib" # The place for user configuration, heap files, etc. if [ -z "$ISABELLE_IDENTIFIER" ]; then ISABELLE_HOME_USER="$USER_HOME/.isabelle" else ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER" fi # Where to look for isabelle tools (multiple dirs separated by ':'). ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" # Location for temporary files (should be on a local file system). ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER" # Heap locations. ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps" ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps" # HTML browser info. ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info" # Site settings check -- just to make it a little bit harder to copy this file verbatim! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } ISABELLE_SITE_SETTINGS_PRESENT=true ### ### Default logic ### ISABELLE_LOGIC=HOL ### ### Docs and external files ### # Where to look for docs (multiple dirs separated by ':'). ISABELLE_DOCS="$ISABELLE_HOME/doc" ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY" ISABELLE_DOCS_EXAMPLES="~~/src/HOL/Examples/Seq.thy:~~/src/HOL/Examples/Drinker.thy:~~/src/HOL/Examples/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML" # "open" within desktop environment (potentially asynchronous) case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_OPEN="xdg-open" ;; macos) ISABELLE_OPEN="open" ;; windows) ISABELLE_OPEN="cygstart" ;; esac PDF_VIEWER="$ISABELLE_OPEN" ISABELLE_EXTERNAL_FILES="bmp:eps:gif:jpeg:jpg:pdf:png:xmp" ### ### Symbol rendering ### ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols" ### ### OCaml ### ISABELLE_OPAM_ROOT="$USER_HOME/.opam" ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.12.0" ### ### Haskell ### ISABELLE_STACK_ROOT="$USER_HOME/.stack" ISABELLE_STACK_RESOLVER="lts-17.10" ISABELLE_GHC_VERSION="ghc-8.10.4" ### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_MLTON="/usr/bin/mlton" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/src/Doc/Tutorial/document/build b/src/Doc/Tutorial/document/build --- a/src/Doc/Tutorial/document/build +++ b/src/Doc/Tutorial/document/build @@ -1,13 +1,10 @@ #!/usr/bin/env bash 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 --git a/src/Doc/Tutorial/document/isa-index b/src/Doc/Tutorial/document/isa-index --- a/src/Doc/Tutorial/document/isa-index +++ b/src/Doc/Tutorial/document/isa-index @@ -1,23 +1,23 @@ #! /bin/sh # #sedindex - shell script to create indexes, preprocessing LaTeX's .idx file # # puts strings prefixed by * into \tt font # terminator characters for strings are |!@{} # # a space terminates the \tt part to allow \index{*notE theorem}, etc. # # note that makeindex uses a dboule quote (") to delimit special characters. # # change *"X"Y"Z"W to "X"Y"Z"W@{\tt "X"Y"Z"W} # change *"X"Y"Z to "X"Y"Z@{\tt "X"Y"Z} # change *"X"Y to "X"Y@{\tt "X"Y} # change *"X to "X@{\tt "X} # change *IDENT to IDENT@{\tt IDENT} # where IDENT is any string not containing | ! or @ # FOUR backslashes: to escape the shell AND sed sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g 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 --git a/src/Doc/prepare_document b/src/Doc/prepare_document --- a/src/Doc/prepare_document +++ b/src/Doc/prepare_document @@ -1,21 +1,19 @@ #!/usr/bin/env bash 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 --git a/src/Doc/sedindex b/src/Doc/sedindex --- a/src/Doc/sedindex +++ b/src/Doc/sedindex @@ -1,21 +1,21 @@ #! /bin/sh # #sedindex - shell script to create indexes, preprocessing LaTeX's .idx file # # puts strings prefixed by * into \tt font # terminator characters for strings are |!@{} # # a space terminates the \tt part to allow \index{*NE theorem}, etc. # # change *"X"Y"Z"W to "X"Y"Z"W@{\tt "X"Y"Z"W} # change *"X"Y"Z to "X"Y"Z@{\tt "X"Y"Z} # change *"X"Y to "X"Y@{\tt "X"Y} # change *"X to "X@{\tt "X} # change *IDENT to IDENT@{\tt IDENT} # where IDENT is any string not containing | ! or @ # FOUR backslashes: to escape the shell AND sed sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\tt \1}~g 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