# HG changeset patch # User wenzelm # Date 1621434910 -7200 # Node ID 8c460c09665eb0a83ca15354d8c49ecc59babcc8 # Parent b2d47981c8dc751f9ad53e0369183ec1c7c56282 prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document; diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Classes/document/build --- a/src/Doc/Classes/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Corec/document/build --- a/src/Doc/Corec/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Datatypes/document/build --- a/src/Doc/Datatypes/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Eisbach/document/build --- a/src/Doc/Eisbach/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Functions/document/build --- a/src/Doc/Functions/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Implementation/document/build --- a/src/Doc/Implementation/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Isar_Ref/document/build --- a/src/Doc/Isar_Ref/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r b2d47981c8dc -r 8c460c09665e src/Doc/JEdit/document/build --- a/src/Doc/JEdit/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Locales/document/build --- a/src/Doc/Locales/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Nitpick/document/build --- a/src/Doc/Nitpick/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Prog_Prove/document/build --- a/src/Doc/Prog_Prove/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff -r b2d47981c8dc -r 8c460c09665e src/Doc/ROOT --- a/src/Doc/ROOT Wed May 19 15:53:55 2021 +0200 +++ b/src/Doc/ROOT Wed May 19 16:35:10 2021 +0200 @@ -1,19 +1,17 @@ chapter Doc session Classes (doc) in "Classes" = HOL + - options [document_logo = "Isar", document_bibliography, document_build = "build", + options [document_logo = "Isar", document_bibliography, document_variants = "classes", quick_and_dirty] theories [document = false] Setup theories Classes document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files - "build" "root.tex" "style.sty" @@ -46,23 +44,21 @@ "style.sty" session Corec (doc) in "Corec" = Datatypes + - options [document_build = "build", document_bibliography, document_variants = "corec"] + options [document_bibliography, document_variants = "corec"] theories Corec document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files - "build" "root.tex" "style.sty" session Datatypes (doc) in "Datatypes" = HOL + - options [document_build = "build", document_bibliography, document_variants = "datatypes"] + options [document_bibliography, document_variants = "datatypes"] sessions "HOL-Library" theories [document = false] @@ -70,21 +66,18 @@ theories Datatypes document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files - "build" "root.tex" "style.sty" session Eisbach (doc) in "Eisbach" = HOL + - options [document_logo = "Eisbach", document_bibliography, document_build = "build", - document_variants = "eisbach", quick_and_dirty, - print_mode = "no_brackets,iff", show_question_marks = false] + options [document_logo = "Eisbach", document_bibliography, document_variants = "eisbach", + quick_and_dirty, print_mode = "no_brackets,iff", show_question_marks = false] sessions "HOL-Eisbach" theories [document = false] @@ -93,7 +86,6 @@ Preface Manual document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" @@ -102,23 +94,20 @@ "underscore.sty" "manual.bib" document_files - "build" "root.tex" "style.sty" session Functions (doc) in "Functions" = HOL + - options [document_build = "build", document_bibliography, document_variants = "functions", + options [document_bibliography, document_variants = "functions", skip_proofs = false, quick_and_dirty] theories Functions document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files - "build" "conclusion.tex" "intro.tex" "root.tex" @@ -151,7 +140,7 @@ "root.tex" session Implementation (doc) in "Implementation" = HOL + - options [document_logo = "Isar", document_bibliography, document_build = "build", + options [document_logo = "Isar", document_bibliography, document_variants = "implementation", quick_and_dirty] theories Eq @@ -166,7 +155,6 @@ theories [parallel_proofs = 0] Logic document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" @@ -175,13 +163,12 @@ "underscore.sty" "manual.bib" document_files - "build" "root.tex" "style.sty" session Isar_Ref (doc) in "Isar_Ref" = HOL + - options [document_logo = "Isar", document_bibliography, document_build = "build", - document_variants = "isar-ref", quick_and_dirty, thy_output_source] + options [document_logo = "Isar", document_bibliography, document_variants = "isar-ref", + quick_and_dirty, thy_output_source] sessions "HOL-Library" theories @@ -200,7 +187,6 @@ Quick_Reference Symbols document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" @@ -209,15 +195,14 @@ "underscore.sty" "manual.bib" document_files - "build" "isar-vm.pdf" "isar-vm.svg" "root.tex" "style.sty" session JEdit (doc) in "JEdit" = HOL + - options [document_logo = "jEdit", document_bibliography, document_build = "build", - document_variants = "jedit", thy_output_source] + options [document_logo = "jEdit", document_bibliography, document_variants = "jedit", + thy_output_source] theories JEdit document_files (in "..") @@ -226,7 +211,6 @@ "isar.sty" "manual.bib" "pdfsetup.sty" - "prepare_document" "ttbox.sty" "underscore.sty" document_files (in "../Isar_Ref/document") @@ -234,7 +218,6 @@ document_files "auto-tools.png" "bibtex-mode.png" - "build" "cite-completion.png" "isabelle-jedit.png" "markdown-document.png" @@ -254,30 +237,26 @@ "theories.png" session Sugar (doc) in "Sugar" = HOL + - options [document_build = "build", document_bibliography, document_variants = "sugar"] + options [document_bibliography, document_variants = "sugar"] sessions "HOL-Library" theories Sugar document_files (in "..") - "prepare_document" "pdfsetup.sty" document_files - "build" "root.bib" "root.tex" session Locales (doc) in "Locales" = HOL + - options [document_build = "build", document_bibliography, - document_variants = "locales", thy_output_margin = 65, skip_proofs = false] + options [document_bibliography, document_variants = "locales", + thy_output_margin = 65, skip_proofs = false] theories Examples1 Examples2 Examples3 document_files (in "..") - "prepare_document" "pdfsetup.sty" document_files - "build" "root.bib" "root.tex" @@ -336,20 +315,17 @@ "root.tex" session Nitpick (doc) in "Nitpick" = Pure + - options [document_logo = "Nitpick", document_bibliography, document_build = "build", - document_variants = "nitpick"] + options [document_logo = "Nitpick", document_bibliography, document_variants = "nitpick"] document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "manual.bib" document_files - "build" "root.tex" session Prog_Prove (doc) in "Prog_Prove" = HOL + - options [document_logo = "HOL", document_bibliography, document_build = "build", - document_variants = "prog-prove", show_question_marks = false] + options [document_logo = "HOL", document_bibliography, document_variants = "prog-prove", + show_question_marks = false] theories Basics Bool_nat_list @@ -360,11 +336,9 @@ document_files (in ".") "MyList.thy" document_files (in "..") - "prepare_document" "pdfsetup.sty" document_files "bang.pdf" - "build" "intro-isabelle.tex" "prelude.tex" "root.bib" @@ -372,20 +346,17 @@ "svmono.cls" session Sledgehammer (doc) in "Sledgehammer" = Pure + - options [document_logo = "S/H", document_bibliography, document_build = "build", - document_variants = "sledgehammer"] + options [document_logo = "S/H", document_bibliography, document_variants = "sledgehammer"] document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "manual.bib" document_files - "build" "root.tex" session System (doc) in "System" = Pure + - options [document_logo = "_", document_bibliography, document_build = "build", - document_variants = "system", thy_output_source] + options [document_logo = "_", document_bibliography, document_variants = "system", + thy_output_source] sessions "HOL-Library" theories @@ -397,7 +368,6 @@ Phabricator Misc document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" @@ -408,7 +378,6 @@ document_files (in "../Isar_Ref/document") "style.sty" document_files - "build" "root.tex" session Tutorial (doc) in "Tutorial" = HOL + @@ -506,8 +475,7 @@ "types0.tex" session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL + - options [document_logo = "Isar", document_bibliography, document_build = "build", - document_variants = "typeclass_hierarchy"] + options [document_logo = "Isar", document_bibliography, document_variants = "typeclass_hierarchy"] sessions "HOL-Library" theories [document = false] @@ -515,13 +483,11 @@ theories Typeclass_Hierarchy document_files (in "..") - "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files - "build" "root.tex" "style.sty" diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Sledgehammer/document/build --- a/src/Doc/Sledgehammer/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r b2d47981c8dc -r 8c460c09665e src/Doc/Sugar/document/build --- a/src/Doc/Sugar/document/build Wed May 19 15:53:55 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" -