# HG changeset patch
# User wenzelm
# Date 1671886464 -3600
# Node ID 0438622a7b9cadc400a9eaa604bfa2aa6efdc1ac
# Parent  40c8275f01316b4d55bc8b1602d4c21be9949e3c
clarified messages;

diff -r 40c8275f0131 -r 0438622a7b9c src/Pure/Thy/document_build.scala
--- 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
diff -r 40c8275f0131 -r 0438622a7b9c src/Tools/jEdit/src/document_dockable.scala
--- 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 =