--- a/src/Pure/Thy/document_build.scala Wed May 19 12:53:51 2021 +0200
+++ b/src/Pure/Thy/document_build.scala Wed May 19 13:19:37 2021 +0200
@@ -170,6 +170,8 @@
def session: String = info.name
def options: Options = info.options
+ def document_bibliography: Boolean = options.bool("document_bibliography")
+
def document_preprocessor: Option[String] =
proper_string(options.string("document_preprocessor"))
@@ -355,8 +357,11 @@
" " + directory.root_name_script() + "\n"
def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String =
- directory.conditional_script("bib", "$ISABELLE_BIBTEX",
+ {
+ val ext = if (context.document_bibliography) "aux" else "bib"
+ directory.conditional_script(ext, "$ISABELLE_BIBTEX",
after = if (latex) latex_script(context, directory) else "")
+ }
def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String =
directory.conditional_script("idx", "$ISABELLE_MAKEINDEX",