# HG changeset patch
# User wenzelm
# Date 1667650117 -3600
# Node ID 87cd8506e000a31cfdeb75c15473e93d6ee44d2f
# Parent  107d8203fbd7a1bb8e147820627b69eea48b2ce5
document_build engine for "lipics", with options and document_files;

diff -r 107d8203fbd7 -r 87cd8506e000 etc/build.props
--- a/etc/build.props	Sat Nov 05 12:29:22 2022 +0100
+++ b/etc/build.props	Sat Nov 05 13:08:37 2022 +0100
@@ -297,6 +297,7 @@
   isabelle.Bash$Handler \
   isabelle.Bibtex$File_Format \
   isabelle.Document_Build$Build_Engine \
+  isabelle.Document_Build$LIPIcs_Engine \
   isabelle.Document_Build$LuaLaTeX_Engine \
   isabelle.Document_Build$PDFLaTeX_Engine \
   isabelle.CI_Builds \
diff -r 107d8203fbd7 -r 87cd8506e000 src/Doc/Demo_LIPIcs/ROOT
--- a/src/Doc/Demo_LIPIcs/ROOT	Sat Nov 05 12:29:22 2022 +0100
+++ b/src/Doc/Demo_LIPIcs/ROOT	Sat Nov 05 13:08:37 2022 +0100
@@ -2,13 +2,9 @@
 
 session Demo_LIPIcs (doc) = HOL +
   options [document_variants = "demo_lipics",
-    document_build = "pdflatex", document_heading_prefix = "", document_comment_latex]
+    document_build = "lipics"]
   theories
     Document
-  document_files (in "$ISABELLE_LIPICS_HOME")
-    "cc-by.pdf"
-    "lipics-logo-bw.pdf"
-    "lipics-v2021.cls"
   document_files
     "root.bib"
     "root.tex"
diff -r 107d8203fbd7 -r 87cd8506e000 src/Pure/Admin/build_lipics.scala
--- a/src/Pure/Admin/build_lipics.scala	Sat Nov 05 12:29:22 2022 +0100
+++ b/src/Pure/Admin/build_lipics.scala	Sat Nov 05 13:08:37 2022 +0100
@@ -14,6 +14,13 @@
 
 
 object Build_LIPIcs {
+  /* files for document preparation */
+
+  val document_files: List[Path] =
+    for (name <- List("cc-by.pdf", "lipics-logo-bw.pdf", "lipics-v2021.cls"))
+      yield Path.explode("$ISABELLE_LIPICS_HOME/" + name)
+
+
   /* build lipics component */
 
   val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz"
diff -r 107d8203fbd7 -r 87cd8506e000 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sat Nov 05 12:29:22 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Sat Nov 05 13:08:37 2022 +0100
@@ -217,12 +217,15 @@
 
     /* document directory */
 
+    def make_directory(dir: Path, doc: Document_Variant): Path =
+      Isabelle_System.make_directory(dir + Path.basic(doc.name))
+
     def prepare_directory(
       dir: Path,
       doc: Document_Variant,
       latex_output: Latex.Output
     ): Directory = {
-      val doc_dir = Isabelle_System.make_directory(dir + Path.basic(doc.name))
+      val doc_dir = make_directory(dir, doc)
 
 
       /* actual sources: with SHA1 digest */
@@ -383,6 +386,21 @@
   class PDFLaTeX_Engine extends Bash_Engine("pdflatex") { override def use_pdflatex: Boolean = true }
   class Build_Engine extends Bash_Engine("build") { override def use_build_script: Boolean = true }
 
+  class LIPIcs_Engine extends Bash_Engine("lipics") {
+    def lipics_options(options: Options): Options =
+      options + "document_heading_prefix=" + "document_comment_latex"
+
+    override def use_pdflatex: Boolean = true
+
+    override def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory = {
+      val doc_dir = context.make_directory(dir, doc)
+      Build_LIPIcs.document_files.foreach(Isabelle_System.copy_file(_, doc_dir))
+
+      val latex_output = new Latex.Output(lipics_options(context.options))
+      context.prepare_directory(dir, doc, latex_output)
+    }
+  }
+
 
   /* build documents */