# HG changeset patch
# User wenzelm
# Date 1621584938 -7200
# Node ID 74078d50d77b356479d2106455b41c50e4fc21ab
# Parent  736c1b239b9d1eb31e1e491e59c4a1b0e2c63f00
clarified signature: avoid dispatch via name;

diff -r 736c1b239b9d -r 74078d50d77b 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 */