src/Pure/Thy/document_build.scala
changeset 76769 0438622a7b9c
parent 76758 8fc7157485d8
child 76826 eb3b946bdeff
equal deleted inserted replaced
76768:40c8275f0131 76769:0438622a7b9c
   130 
   130 
   131   val isabelle_styles: List[Path] =
   131   val isabelle_styles: List[Path] =
   132     List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
   132     List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
   133       map(name => texinputs + Path.basic(name))
   133       map(name => texinputs + Path.basic(name))
   134 
   134 
       
   135   def running_script(title: String): String = "echo 'Running " + quote(title) + " ...'; "
       
   136   def is_running_script(msg: String): Boolean =
       
   137     msg.startsWith("Running \"") && msg.endsWith("\" ...")
       
   138 
   135   sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) {
   139   sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) {
   136     def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)
   140     def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)
   137     def file_pos: String = name.path.implode_symbolic
   141     def file_pos: String = name.path.implode_symbolic
   138     def write(latex_output: Latex.Output, dir: Path): Unit =
   142     def write(latex_output: Latex.Output, dir: Path): Unit =
   139       content.output(latex_output(_, file_pos = file_pos)).write(dir)
   143       content.output(latex_output(_, file_pos = file_pos)).write(dir)
   302     sources: SHA1.Digest
   306     sources: SHA1.Digest
   303   ) {
   307   ) {
   304     def root_name_script(ext: String = ""): String =
   308     def root_name_script(ext: String = ""): String =
   305       Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext)
   309       Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext)
   306 
   310 
   307     def conditional_script(ext: String, exe: String, after: String = ""): String =
   311     def conditional_script(
       
   312       ext: String, exe: String, title: String = "", after: String = ""
       
   313     ): String = {
   308       "if [ -f " + root_name_script(ext) + " ]\n" +
   314       "if [ -f " + root_name_script(ext) + " ]\n" +
   309       "then\n" +
   315       "then\n" +
   310       "  " + exe + " " + root_name_script() + "\n" +
   316       "  " + (if (title.nonEmpty) running_script(title) else "") +
       
   317         exe + " " + root_name_script() + "\n" +
   311       (if (after.isEmpty) "" else "  " + after) +
   318       (if (after.isEmpty) "" else "  " + after) +
   312       "fi\n"
   319       "fi\n"
       
   320     }
   313 
   321 
   314     def log_errors(): List[String] =
   322     def log_errors(): List[String] =
   315       Latex.latex_errors(doc_dir, root_name) :::
   323       Latex.latex_errors(doc_dir, root_name) :::
   316       Bibtex.bibtex_errors(doc_dir, root_name)
   324       Bibtex.bibtex_errors(doc_dir, root_name)
   317 
   325 
   348   abstract class Bash_Engine(name: String) extends Engine(name) {
   356   abstract class Bash_Engine(name: String) extends Engine(name) {
   349     def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory =
   357     def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory =
   350       context.prepare_directory(dir, doc, new Latex.Output(context.options))
   358       context.prepare_directory(dir, doc, new Latex.Output(context.options))
   351 
   359 
   352     def use_pdflatex: Boolean = false
   360     def use_pdflatex: Boolean = false
       
   361     def running_latex: String = running_script(if (use_pdflatex) "pdflatex" else "lualatex")
   353     def latex_script(context: Context, directory: Directory): String =
   362     def latex_script(context: Context, directory: Directory): String =
   354       (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
   363       running_latex + (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
   355         " " + directory.root_name_script() + "\n"
   364         " " + directory.root_name_script() + "\n"
   356 
   365 
   357     def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String = {
   366     def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String = {
   358       val ext = if (context.document_bibliography) "aux" else "bib"
   367       val ext = if (context.document_bibliography) "aux" else "bib"
   359       directory.conditional_script(ext, "$ISABELLE_BIBTEX",
   368       directory.conditional_script(ext, "$ISABELLE_BIBTEX", title = "bibtex",
   360         after = if (latex) latex_script(context, directory) else "")
   369         after = if (latex) latex_script(context, directory) else "")
   361     }
   370     }
   362 
   371 
   363     def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String =
   372     def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String =
   364       directory.conditional_script("idx", "$ISABELLE_MAKEINDEX",
   373       directory.conditional_script("idx", "$ISABELLE_MAKEINDEX", title = "makeindex",
   365         after = if (latex) latex_script(context, directory) else "")
   374         after = if (latex) latex_script(context, directory) else "")
   366 
   375 
   367     def use_build_script: Boolean = false
   376     def use_build_script: Boolean = false
   368     def build_script(context: Context, directory: Directory): String = {
   377     def build_script(context: Context, directory: Directory): String = {
   369       val has_build_script = (directory.doc_dir + Path.explode("build")).is_file
   378       val has_build_script = (directory.doc_dir + Path.explode("build")).is_file