--- a/src/Pure/Thy/document_build.scala Sat Dec 24 13:19:39 2022 +0100
+++ b/src/Pure/Thy/document_build.scala Sat Dec 24 13:54:24 2022 +0100
@@ -132,6 +132,10 @@
List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
map(name => texinputs + Path.basic(name))
+ def running_script(title: String): String = "echo 'Running " + quote(title) + " ...'; "
+ def is_running_script(msg: String): Boolean =
+ msg.startsWith("Running \"") && msg.endsWith("\" ...")
+
sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) {
def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)
def file_pos: String = name.path.implode_symbolic
@@ -304,12 +308,16 @@
def root_name_script(ext: String = ""): String =
Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext)
- def conditional_script(ext: String, exe: String, after: String = ""): String =
+ def conditional_script(
+ ext: String, exe: String, title: String = "", after: String = ""
+ ): String = {
"if [ -f " + root_name_script(ext) + " ]\n" +
"then\n" +
- " " + exe + " " + root_name_script() + "\n" +
+ " " + (if (title.nonEmpty) running_script(title) else "") +
+ exe + " " + root_name_script() + "\n" +
(if (after.isEmpty) "" else " " + after) +
"fi\n"
+ }
def log_errors(): List[String] =
Latex.latex_errors(doc_dir, root_name) :::
@@ -350,18 +358,19 @@
context.prepare_directory(dir, doc, new Latex.Output(context.options))
def use_pdflatex: Boolean = false
+ def running_latex: String = running_script(if (use_pdflatex) "pdflatex" else "lualatex")
def latex_script(context: Context, directory: Directory): String =
- (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
+ running_latex + (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
" " + directory.root_name_script() + "\n"
def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String = {
val ext = if (context.document_bibliography) "aux" else "bib"
- directory.conditional_script(ext, "$ISABELLE_BIBTEX",
+ directory.conditional_script(ext, "$ISABELLE_BIBTEX", title = "bibtex",
after = if (latex) latex_script(context, directory) else "")
}
def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String =
- directory.conditional_script("idx", "$ISABELLE_MAKEINDEX",
+ directory.conditional_script("idx", "$ISABELLE_MAKEINDEX", title = "makeindex",
after = if (latex) latex_script(context, directory) else "")
def use_build_script: Boolean = false
--- a/src/Tools/jEdit/src/document_dockable.scala Sat Dec 24 13:19:39 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Sat Dec 24 13:54:24 2022 +0100
@@ -106,7 +106,7 @@
}
private val scroll_log_area = new ScrollPane(log_area)
- def log_progress(): Document_Editor.Log_Progress =
+ def log_progress(only_running: Boolean = false): Document_Editor.Log_Progress =
new Document_Editor.Log_Progress(PIDE.session) {
override def show(text: String): Unit =
if (text != log_area.text) {
@@ -114,6 +114,8 @@
val vertical = scroll_log_area.peer.getVerticalScrollBar
vertical.setValue(vertical.getMaximum)
}
+ override def echo(msg: String): Unit =
+ if (!only_running || Document_Build.is_running_script(msg)) super.echo(msg)
}
@@ -131,11 +133,13 @@
private def finish_process(output: List[XML.Tree]): Unit =
current_state.change(_.finish(output))
- private def run_process(body: Document_Editor.Log_Progress => Unit): Boolean = {
+ private def run_process(only_running: Boolean = false)(
+ body: Document_Editor.Log_Progress => Unit
+ ): Boolean = {
val started =
current_state.change_result { st =>
if (st.process.is_finished) {
- val progress = log_progress()
+ val progress = log_progress(only_running = only_running)
val process =
Future.thread[Unit](name = "Document_Dockable.process") {
await_process()
@@ -151,7 +155,7 @@
private def load_document(session: String): Boolean = {
val options = PIDE.options.value
- run_process { _ =>
+ run_process() { _ =>
try {
val session_background =
Document_Build.session_background(
@@ -212,7 +216,7 @@
private def build_document(): Unit = {
PIDE.editor.document_session() match {
case Some(session_background) if session_background.info.documents.nonEmpty =>
- run_process { progress =>
+ run_process(only_running = true) { progress =>
show_page(log_page)
val result = Exn.capture { document_build(session_background, progress) }
val msgs =