--- 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 \
--- 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"
--- 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"
--- 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 */