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 |