# HG changeset patch
# User wenzelm
# Date 1621368141 -7200
# Node ID 26cd26aaf108bf514fed3a44213ad75539376be9
# Parent  f7f0d516df0c527c6e336fad4bda5d56cfd1a1d7
option document_preprocessor;

diff -r f7f0d516df0c -r 26cd26aaf108 NEWS
--- 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.
diff -r f7f0d516df0c -r 26cd26aaf108 etc/options
--- 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 = ""
diff -r f7f0d516df0c -r 26cd26aaf108 src/Doc/System/Sessions.thy
--- 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
diff -r f7f0d516df0c -r 26cd26aaf108 src/Pure/Thy/document_build.scala
--- 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)