# HG changeset patch
# User wenzelm
# Date 1636386522 -3600
# Node ID 255e651a4c5f6f50410cb95fb927f4f1398ce93e
# Parent  015282fb3e31cabdb42866a3746e0088ffd8e867
discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do;

diff -r 015282fb3e31 -r 255e651a4c5f NEWS
--- a/NEWS	Mon Nov 08 13:51:24 2021 +0100
+++ b/NEWS	Mon Nov 08 16:48:42 2021 +0100
@@ -95,11 +95,6 @@
 specifies the name of the logo variant, while "_" (underscore) refers to
 the unnamed variant. The output file name is always "isabelle_logo.pdf".
 
-* 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.
-
 * Option "document_build" determines the document build engine, as
 defined in Isabelle/Scala (as system service). The subsequent engines
 are provided by the Isabelle distribution:
diff -r 015282fb3e31 -r 255e651a4c5f etc/options
--- a/etc/options	Mon Nov 08 13:51:24 2021 +0100
+++ b/etc/options	Mon Nov 08 16:48:42 2021 +0100
@@ -17,8 +17,6 @@
   -- "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"
   -- "document build engine (e.g. lualatex, pdflatex, build)"
 option document_logo : string = ""
diff -r 015282fb3e31 -r 255e651a4c5f src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Nov 08 13:51:24 2021 +0100
+++ b/src/Doc/System/Sessions.thy	Mon Nov 08 16:48:42 2021 +0100
@@ -243,12 +243,6 @@
     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
-    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 015282fb3e31 -r 255e651a4c5f src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Nov 08 13:51:24 2021 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Nov 08 16:48:42 2021 +0100
@@ -185,9 +185,6 @@
 
     def document_bibliography: Boolean = options.bool("document_bibliography")
 
-    def document_preprocessor: Option[String] =
-      proper_string(options.string("document_preprocessor"))
-
     def document_logo: Option[String] =
       options.string("document_logo") match {
         case "" => None
@@ -275,16 +272,6 @@
       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)