--- a/NEWS Tue May 18 21:09:51 2021 +0200
+++ b/NEWS Tue May 18 22:02:21 2021 +0200
@@ -56,6 +56,11 @@
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
adjust session ROOT options.
+* Option "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 allows to
+apply adhoc patches, without requiring a separate "build" script.
+
* Isabelle .sty files are automatically generated within the document
output directory; former "isabelle latex -o sty" has been discontinued.
Minor INCOMPATIBILITY in document build scripts.
--- a/etc/options Tue May 18 21:09:51 2021 +0200
+++ b/etc/options Tue May 18 22:02:21 2021 +0200
@@ -13,6 +13,8 @@
-- "alternative document variants (separated by colons)"
option document_tags : string = ""
-- "default command tags (separated by commas)"
+option document_preprocessor : string = ""
+ -- "document preprocessor: executable relative to document output directory"
option document_build : string = "lualatex"
-- "document build engine (e.g. lualatex, pdflatex, build)"
option document_logo : string = ""
--- a/src/Doc/System/Sessions.thy Tue May 18 21:09:51 2021 +0200
+++ b/src/Doc/System/Sessions.thy Tue May 18 22:02:21 2021 +0200
@@ -238,6 +238,12 @@
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_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
+ allows to apply adhoc patches, without requiring a separate \<^verbatim>\<open>build\<close>
+ script.
+
\<^item> @{system_option_def "threads"} determines the number of worker threads
for parallel checking of theories and proofs. The default \<open>0\<close> means that a
sensible maximum value is determined by the underlying hardware. For
--- a/src/Pure/Thy/document_build.scala Tue May 18 21:09:51 2021 +0200
+++ b/src/Pure/Thy/document_build.scala Tue May 18 22:02:21 2021 +0200
@@ -170,6 +170,9 @@
def session: String = info.name
def options: Options = info.options
+ def document_preprocessor: Option[String] =
+ proper_string(options.string("document_preprocessor"))
+
def document_logo: Option[String] =
options.string("document_logo") match {
case "" => None
@@ -256,6 +259,16 @@
val root_name1 = "root_" + doc.name
val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
+ for (name <- document_preprocessor) {
+ def message(s: String): String = s + " for document_preprocessor=" + quote(name)
+ val path = doc_dir + Path.explode(name)
+ if (path.is_file) {
+ try { Isabelle_System.bash(File.bash_path(path), cwd = doc_dir.file).check }
+ catch { case ERROR(msg) => cat_error(msg, message("The error(s) above occurred")) }
+ }
+ else error(message("Missing executable"))
+ }
+
val digests1 = List(doc.print, document_logo.toString, document_build).map(SHA1.digest)
val digests2 = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
val sources = SHA1.digest_set(digests1 ::: digests2)