clarified signature: avoid dispatch via name;
authorwenzelm
Fri, 21 May 2021 10:15:38 +0200
changeset 74015 74078d50d77b
parent 74014 736c1b239b9d
child 74016 f4be1b0d7a51
clarified signature: avoid dispatch via name;
src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Thu May 20 23:33:54 2021 +0200
+++ b/src/Pure/Thy/document_build.scala	Fri May 21 10:15:38 2021 +0200
@@ -352,8 +352,9 @@
     def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory =
       context.prepare_directory(dir, doc)
 
+    def use_pdflatex: Boolean = false
     def latex_script(context: Context, directory: Directory): String =
-      (if (name == "pdflatex") "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
+      (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
         " " + directory.root_name_script() + "\n"
 
     def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String =
@@ -367,17 +368,17 @@
       directory.conditional_script("idx", "$ISABELLE_MAKEINDEX",
         after = if (latex) latex_script(context, directory) else "")
 
+    def use_build_script: Boolean = false
     def build_script(context: Context, directory: Directory): String =
     {
-      val build_required = name == "build"
-      val build_provided = (directory.doc_dir + Path.explode("build")).is_file
+      val has_build_script = (directory.doc_dir + Path.explode("build")).is_file
 
-      if (!build_required && build_provided) {
+      if (!use_build_script && has_build_script) {
         error("Unexpected document build script for option document_build=" +
           quote(context.document_build))
       }
-      else if (build_required && !build_provided) error("Missing document build script")
-      else if (build_required) "./build pdf " + Bash.string(directory.doc.name)
+      else if (use_build_script && !has_build_script) error("Missing document build script")
+      else if (has_build_script) "./build pdf " + Bash.string(directory.doc.name)
       else {
         "set -e\n" +
         latex_script(context, directory) +
@@ -404,8 +405,8 @@
   }
 
   class LuaLaTeX_Engine extends Bash_Engine("lualatex")
-  class PDFLaTeX_Engine extends Bash_Engine("pdflatex")
-  class Build_Engine extends Bash_Engine("build")
+  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 }
 
 
   /* build documents */