# HG changeset patch
# User wenzelm
# Date 1621287025 -7200
# Node ID 52030acb19acf5480f9b2e1b4bb914c64333df49
# Parent  7c2f7688a5a86470027c63db0163a8f1cc7db86e
option document_build refers to build engine in Isabelle/Scala;
pdflatex is back as legacy build engine, e.g. for published proceedings;

diff -r 7c2f7688a5a8 -r 52030acb19ac NEWS
--- a/NEWS	Mon May 17 20:37:42 2021 +0200
+++ b/NEWS	Mon May 17 23:30:25 2021 +0200
@@ -34,6 +34,23 @@
 
 *** Document preparation ***
 
+* Option "document_build" determines the document build engine, as
+defined in Isabelle/Scala (as system service). The subsequent engines
+are provided by the Isabelle distribution:
+
+  . "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX
+    build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX
+
+  . "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for
+    special LaTeX styles)
+
+  . "build": delegate to the executable "./build pdf", using
+    ISABELLE_LUALATEX by default
+
+The presence of a "build" command within the document output directory
+explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
+adjust session ROOT options.
+
 * Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
 \guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
 (which is now also the default in "isabelle mkroot").
diff -r 7c2f7688a5a8 -r 52030acb19ac etc/options
--- a/etc/options	Mon May 17 20:37:42 2021 +0200
+++ b/etc/options	Mon May 17 23:30:25 2021 +0200
@@ -13,6 +13,8 @@
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
+option document_build : string = "lualatex"
+  -- "document build engine (e.g. lualatex, pdflatex, build)"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
diff -r 7c2f7688a5a8 -r 52030acb19ac etc/settings
--- a/etc/settings	Mon May 17 20:37:42 2021 +0200
+++ b/etc/settings	Mon May 17 23:30:25 2021 +0200
@@ -34,6 +34,10 @@
 isabelle_scala_service 'isabelle.Simplifier_Trace$Handler'
 isabelle_scala_service 'isabelle.Server_Commands'
 
+isabelle_scala_service 'isabelle.Document_Build$LuaLaTeX_Engine'
+isabelle_scala_service 'isabelle.Document_Build$PDFLaTeX_Engine'
+isabelle_scala_service 'isabelle.Document_Build$Build_Engine'
+
 #paranoia settings -- avoid intrusion of alien options
 unset "_JAVA_OPTIONS"
 unset "JAVA_TOOL_OPTIONS"
@@ -57,10 +61,16 @@
 
 
 ###
-### Document preparation (cf. isabelle latex/document)
+### Document preparation (cf. isabelle latex)
 ###
 
-ISABELLE_PDFLATEX="lualatex --file-line-error"
+if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
+  ISABELLE_PDFLATEX="pdflatex -c-style-errors"
+else
+  ISABELLE_PDFLATEX="pdflatex -file-line-error"
+fi
+
+ISABELLE_LUALATEX="lualatex --file-line-error"
 ISABELLE_BIBTEX="bibtex"
 ISABELLE_MAKEINDEX="makeindex"
 ISABELLE_EPSTOPDF="epstopdf"
diff -r 7c2f7688a5a8 -r 52030acb19ac src/Doc/ROOT
--- a/src/Doc/ROOT	Mon May 17 20:37:42 2021 +0200
+++ b/src/Doc/ROOT	Mon May 17 23:30:25 2021 +0200
@@ -1,7 +1,7 @@
 chapter Doc
 
 session Classes (doc) in "Classes" = HOL +
-  options [document_variants = "classes", quick_and_dirty]
+  options [document_build = "build", document_variants = "classes", quick_and_dirty]
   theories [document = false] Setup
   theories Classes
   document_files (in "..")
@@ -17,7 +17,7 @@
     "style.sty"
 
 session Codegen (doc) in "Codegen" = HOL +
-  options [document_variants = "codegen", print_mode = "no_brackets,iff"]
+  options [document_build = "build", document_variants = "codegen", print_mode = "no_brackets,iff"]
   sessions
     "HOL-Library"
   theories [document = false]
@@ -44,7 +44,7 @@
     "style.sty"
 
 session Corec (doc) in "Corec" = Datatypes +
-  options [document_variants = "corec"]
+  options [document_build = "build", document_variants = "corec"]
   theories
     Corec
   document_files (in "..")
@@ -60,7 +60,7 @@
     "style.sty"
 
 session Datatypes (doc) in "Datatypes" = HOL +
-  options [document_variants = "datatypes"]
+  options [document_build = "build", document_variants = "datatypes"]
   sessions
     "HOL-Library"
   theories [document = false]
@@ -80,7 +80,7 @@
     "style.sty"
 
 session Eisbach (doc) in "Eisbach" = HOL +
-  options [document_variants = "eisbach", quick_and_dirty,
+  options [document_build = "build", document_variants = "eisbach", quick_and_dirty,
     print_mode = "no_brackets,iff", show_question_marks = false]
   sessions
     "HOL-Eisbach"
@@ -104,7 +104,8 @@
     "style.sty"
 
 session Functions (doc) in "Functions" = HOL +
-  options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
+  options [document_build = "build", document_variants = "functions",
+    skip_proofs = false, quick_and_dirty]
   theories Functions
   document_files (in "..")
     "prepare_document"
@@ -121,7 +122,8 @@
     "style.sty"
 
 session How_to_Prove_it (no_doc) in "How_to_Prove_it" = HOL +
-  options [document_variants = "how_to_prove_it", show_question_marks = false]
+  options [document_build = "build", document_variants = "how_to_prove_it",
+    show_question_marks = false]
   theories
     How_to_Prove_it
   document_files
@@ -130,7 +132,7 @@
     "prelude.tex"
 
 session Intro (doc) in "Intro" = Pure +
-  options [document_variants = "intro"]
+  options [document_build = "build", document_variants = "intro"]
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -146,7 +148,7 @@
     "root.tex"
 
 session Implementation (doc) in "Implementation" = HOL +
-  options [document_variants = "implementation", quick_and_dirty]
+  options [document_build = "build", document_variants = "implementation", quick_and_dirty]
   theories
     Eq
     Integration
@@ -174,7 +176,8 @@
     "style.sty"
 
 session Isar_Ref (doc) in "Isar_Ref" = HOL +
-  options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
+  options [document_build = "build", document_variants = "isar-ref",
+    quick_and_dirty, thy_output_source]
   sessions
     "HOL-Library"
   theories
@@ -210,7 +213,7 @@
     "style.sty"
 
 session JEdit (doc) in "JEdit" = HOL +
-  options [document_variants = "jedit", thy_output_source]
+  options [document_build = "build", document_variants = "jedit", thy_output_source]
   theories
     JEdit
   document_files (in "..")
@@ -247,7 +250,7 @@
     "theories.png"
 
 session Sugar (doc) in "Sugar" = HOL +
-  options [document_variants = "sugar"]
+  options [document_build = "build", document_variants = "sugar"]
   sessions
     "HOL-Library"
   theories Sugar
@@ -260,7 +263,8 @@
     "root.tex"
 
 session Locales (doc) in "Locales" = HOL +
-  options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
+  options [document_build = "build", document_variants = "locales",
+    thy_output_margin = 65, skip_proofs = false]
   theories
     Examples1
     Examples2
@@ -274,7 +278,7 @@
     "root.tex"
 
 session Logics (doc) in "Logics" = Pure +
-  options [document_variants = "logics"]
+  options [document_build = "build", document_variants = "logics"]
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -293,7 +297,7 @@
     "syntax.tex"
 
 session Logics_ZF (doc) in "Logics_ZF" = ZF +
-  options [document_variants = "logics-ZF", print_mode = "brackets",
+  options [document_build = "build", document_variants = "logics-ZF", print_mode = "brackets",
     thy_output_source]
   sessions
     FOL
@@ -319,7 +323,7 @@
     "root.tex"
 
 session Main (doc) in "Main" = HOL +
-  options [document_variants = "main"]
+  options [document_build = "build", document_variants = "main"]
   theories Main_Doc
   document_files (in "..")
     "prepare_document"
@@ -329,7 +333,7 @@
     "root.tex"
 
 session Nitpick (doc) in "Nitpick" = Pure +
-  options [document_variants = "nitpick"]
+  options [document_build = "build", document_variants = "nitpick"]
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -340,7 +344,7 @@
     "root.tex"
 
 session Prog_Prove (doc) in "Prog_Prove" = HOL +
-  options [document_variants = "prog-prove", show_question_marks = false]
+  options [document_build = "build", document_variants = "prog-prove", show_question_marks = false]
   theories
     Basics
     Bool_nat_list
@@ -363,7 +367,7 @@
     "svmono.cls"
 
 session Sledgehammer (doc) in "Sledgehammer" = Pure +
-  options [document_variants = "sledgehammer"]
+  options [document_build = "build", document_variants = "sledgehammer"]
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -374,7 +378,7 @@
     "root.tex"
 
 session System (doc) in "System" = Pure +
-  options [document_variants = "system", thy_output_source]
+  options [document_build = "build", document_variants = "system", thy_output_source]
   sessions
     "HOL-Library"
   theories
@@ -401,7 +405,8 @@
     "root.tex"
 
 session Tutorial (doc) in "Tutorial" = HOL +
-  options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
+  options [document_build = "build", document_variants = "tutorial",
+    print_mode = "brackets", skip_proofs = false]
   directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
     "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
   theories [document = false]
@@ -494,7 +499,7 @@
     "types0.tex"
 
 session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL +
-  options [document_variants = "typeclass_hierarchy"]
+  options [document_build = "build", document_variants = "typeclass_hierarchy"]
   sessions
     "HOL-Library"
   theories [document = false]
diff -r 7c2f7688a5a8 -r 52030acb19ac src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon May 17 20:37:42 2021 +0200
+++ b/src/Pure/Thy/document_build.scala	Mon May 17 23:30:25 2021 +0200
@@ -156,6 +156,14 @@
     def session: String = info.name
     def options: Options = info.options
 
+    def document_build: String = options.string("document_build")
+
+    def get_engine(): Engine =
+    {
+      val name = document_build
+      engines.find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
+    }
+
     def get_export(theory: String, name: String): Export.Entry =
       db_context.get_export(hierarchy, theory, name)
 
@@ -214,8 +222,9 @@
       val root_name1 = "root_" + doc.name
       val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
 
-      val sources =
-        SHA1.digest_set(File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest))
+      val option_digests = List(doc.print, get_engine().name).map(SHA1.digest)
+      val file_digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
+      val sources = SHA1.digest_set(option_digests ::: file_digests)
 
 
       /* derived material */
@@ -270,6 +279,74 @@
   }
 
 
+  /* build engines */
+
+  lazy val engines: List[Engine] = Isabelle_System.make_services(classOf[Engine])
+
+  abstract class Engine(val name: String) extends Isabelle_System.Service
+  {
+    override def toString: String = name
+
+    def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory
+    def build_document(context: Context, directory: Directory, verbose: Boolean): Document_Output
+  }
+
+  abstract class Bash_Engine(name: String) extends Engine(name)
+  {
+    def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory =
+      context.prepare_directory(dir, doc)
+
+    def bash_script(context: Context, directory: Directory): String =
+    {
+      val build_required = name == "build"
+      val build_provided = (directory.doc_dir + Path.explode("build")).is_file
+
+      if (!build_required && build_provided) {
+        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 {
+        def root_bash(ext: String): String = Bash.string(directory.root_name + "." + ext)
+
+        def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
+          "isabelle latex -o " + Bash.string(fmt) + " " + root_bash(ext)
+
+        List(
+          latex_bash(),
+          "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
+          "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
+          latex_bash(),
+          latex_bash()).mkString(" && ")
+      }
+    }
+
+    def build_document(context: Context, directory: Directory, verbose: Boolean): Document_Output =
+    {
+      val settings =
+        if (name == "pdflatex") Nil
+        else List("ISABELLE_PDFLATEX" -> Isabelle_System.getenv("ISABELLE_LUALATEX"))
+
+      val result =
+        context.progress.bash(
+          bash_script(context, directory),
+          cwd = directory.doc_dir.file,
+          env = Isabelle_System.settings() ++ settings,
+          echo = verbose,
+          watchdog = Time.seconds(0.5))
+
+      val log = result.out_lines ::: result.err_lines
+      val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors()
+      directory.make_document(log, errors)
+    }
+  }
+
+  class LuaLaTeX_Engine extends Bash_Engine("lualatex")
+  class PDFLaTeX_Engine extends Bash_Engine("pdflatex")
+  class Build_Engine extends Bash_Engine("build")
+
+
   /* build documents */
 
   def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
@@ -282,10 +359,10 @@
     context: Context,
     output_sources: Option[Path] = None,
     output_pdf: Option[Path] = None,
-    verbose: Boolean = false,
-    verbose_latex: Boolean = false): List[Document_Output] =
+    verbose: Boolean = false): List[Document_Output] =
   {
     val progress = context.progress
+    val engine = context.get_engine()
 
     val documents =
       for (doc <- context.documents)
@@ -295,60 +372,20 @@
           progress.echo("Preparing " + context.session + "/" + doc.name + " ...")
           val start = Time.now()
 
-
-          // prepare directory
-
-          output_sources.foreach(context.prepare_directory(_, doc))
-          val directory = context.prepare_directory(tmp_dir, doc)
-          val doc_dir = directory.doc_dir
-          val root = directory.root_name
-
-
-          // prepare document
+          output_sources.foreach(engine.prepare_directory(context, _, doc))
+          val directory = engine.prepare_directory(context, tmp_dir, doc)
 
-          context.old_document(directory) getOrElse {
-            // bash scripts
-
-            def root_bash(ext: String): String = Bash.string(root + "." + ext)
-
-            def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
-              "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext)
-
-            def bash(items: String*): Process_Result =
-              progress.bash(items.mkString(" && "), cwd = doc_dir.file,
-                echo = verbose_latex, watchdog = Time.seconds(0.5))
-
-
-            // prepare document
+          val document =
+            context.old_document(directory) getOrElse
+              engine.build_document(context, directory, verbose)
 
-            val result =
-              if ((doc_dir + Path.explode("build")).is_file) {
-                bash("./build pdf " + Bash.string(doc.name))
-              }
-              else {
-                bash(
-                  latex_bash(),
-                  "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
-                  "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
-                  latex_bash(),
-                  latex_bash())
-              }
+          val stop = Time.now()
+          val timing = stop - start
 
-            val stop = Time.now()
-            val timing = stop - start
-
-
-            // result
+          progress.echo("Finished " + context.session + "/" + doc.name +
+            " (" + timing.message_hms + " elapsed time)")
 
-            val log = result.out_lines ::: result.err_lines
-            val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors()
-            val document = directory.make_document(log, errors)
-
-            progress.echo("Finished " + context.session + "/" + doc.name +
-              " (" + timing.message_hms + " elapsed time)")
-
-            document
-          }
+          document
         })
       }
 
@@ -429,7 +466,7 @@
         {
           build_documents(context(session, deps, db_context, progress = progress),
             output_sources = output_sources, output_pdf = output_pdf,
-            verbose = true, verbose_latex = verbose_latex)
+            verbose = verbose_latex)
         })
       }
     })