# HG changeset patch
# User wenzelm
# Date 1621423177 -7200
# Node ID 813a08dff3fd71e08106f29ea69cf1886b10579a
# Parent  c31510e70e95c849b0348a5028e7865cd8569d52
explicit option document_bibliography;

diff -r c31510e70e95 -r 813a08dff3fd NEWS
--- a/NEWS	Wed May 19 12:53:51 2021 +0200
+++ b/NEWS	Wed May 19 13:19:37 2021 +0200
@@ -77,6 +77,10 @@
   - Former "isabelle latex -o idx" should be replaced by
     "$ISABELLE_MAKEINDEX root" (without quotes).
 
+* Option "document_bibliography" explicitly enables the use of bibtex;
+the default is to check the presence of root.bib, but it could have a
+different name.
+
 * Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
 \guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
 (which is now also the default in "isabelle mkroot").
diff -r c31510e70e95 -r 813a08dff3fd etc/options
--- a/etc/options	Wed May 19 12:53:51 2021 +0200
+++ b/etc/options	Wed May 19 13:19:37 2021 +0200
@@ -13,6 +13,8 @@
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
+option document_bibliography : bool = false
+  -- "explicitly enable use of bibtex (default: according to presence of root.bib)"
 option document_preprocessor : string = ""
   -- "document preprocessor: executable relative to document output directory"
 option document_build : string = "lualatex"
diff -r c31510e70e95 -r 813a08dff3fd src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed May 19 12:53:51 2021 +0200
+++ b/src/Doc/System/Sessions.thy	Wed May 19 13:19:37 2021 +0200
@@ -238,6 +238,10 @@
     is occasionally useful to control the global visibility of commands via
     session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>).
 
+    \<^item> @{system_option_def "document_bibliography"} explicitly enables the use
+    of \<^verbatim>\<open>bibtex\<close>; the default is to check the presence of \<^verbatim>\<open>root.bib\<close>, but it
+    could have a different name.
+
     \<^item> @{system_option_def "document_preprocessor"} specifies the name of an
     executable that is run within the document output directory, after
     preparing the document sources and before the actual build process. This
diff -r c31510e70e95 -r 813a08dff3fd src/Pure/Thy/document_build.scala
--- 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",