# 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>\ROOT\). + \<^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>\build\ + script. + \<^item> @{system_option_def "threads"} determines the number of worker threads for parallel checking of theories and proofs. The default \0\ 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)