# HG changeset patch
# User wenzelm
# Date 1675283034 -3600
# Node ID 1eb55d6809b3c26de3114779984da8ccc3d92908
# Parent  f1063cdb0093b5fb7b5ad1338cab3b118742e8ec
more general program start message;
progress on "Creating directory";

diff -r f1063cdb0093 -r 1eb55d6809b3 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Wed Feb 01 20:57:15 2023 +0100
+++ b/src/Pure/System/progress.scala	Wed Feb 01 21:23:54 2023 +0100
@@ -85,7 +85,7 @@
 /* structured program progress */
 
 object Program_Progress {
-  class Program private[Program_Progress](title: String) {
+  class Program private[Program_Progress](heading: String, title: String) {
     private val output_buffer = new StringBuffer(256)  // synchronized
 
     def echo(msg: String): Unit = synchronized {
@@ -97,7 +97,7 @@
     private var stop_time: Option[Time] = None
     def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) }
 
-    def output(heading: String): (Command.Results, XML.Body) = synchronized {
+    def output(): (Command.Results, XML.Body) = synchronized {
       val output_text = output_buffer.toString
       val elapsed_time = stop_time.map(t => t - start_time)
 
@@ -127,20 +127,23 @@
   }
 }
 
-abstract class Program_Progress(default_program: String = "program") extends Progress {
+abstract class Program_Progress(
+  default_heading: String = "Running",
+  default_title: String = "program"
+) extends Progress {
   private var _finished_programs: List[Program_Progress.Program] = Nil
   private var _running_program: Option[Program_Progress.Program] = None
 
-  def output(heading: String = "Running"): (Command.Results, XML.Body) = synchronized {
+  def output(): (Command.Results, XML.Body) = synchronized {
     val programs = (_running_program.toList ::: _finished_programs).reverse
-    val programs_output = programs.map(_.output(heading))
+    val programs_output = programs.map(_.output())
     val results = Command.Results.merge(programs_output.map(_._1))
     val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten
     (results, body)
   }
 
-  private def start_program(title: String): Unit = synchronized {
-    _running_program = Some(new Program_Progress.Program(title))
+  private def start_program(heading: String, title: String): Unit = synchronized {
+    _running_program = Some(new Program_Progress.Program(heading, title))
   }
 
   def stop_program(): Unit = synchronized {
@@ -156,12 +159,12 @@
   def detect_program(s: String): Option[String]
 
   override def echo(msg: String): Unit = synchronized {
-    detect_program(msg) match {
-      case Some(title) =>
+    detect_program(msg).map(Word.explode) match {
+      case Some(a :: bs) =>
         stop_program()
-        start_program(title)
-      case None =>
-        if (_running_program.isEmpty) start_program(default_program)
+        start_program(a, Word.implode(bs))
+      case _ =>
+        if (_running_program.isEmpty) start_program(default_heading, default_title)
         _running_program.get.echo(msg)
     }
   }
diff -r f1063cdb0093 -r 1eb55d6809b3 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Feb 01 20:57:15 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Feb 01 21:23:54 2023 +0100
@@ -135,8 +135,8 @@
   def program_start(title: String): String =
     "PROGRAM START \"" + title + "\" ..."
 
-  def program_start_script(title: String): String =
-    "echo " + Bash.string(program_start(title)) + ";"
+  def program_running_script(title: String): String =
+    "echo " + Bash.string(program_start("Running " + title)) + ";"
 
   def detect_program_start(s: String): Option[String] =
     for {
@@ -293,6 +293,8 @@
     ): Directory = {
       val doc_dir = make_directory(dir, doc)
 
+      progress.echo(program_start("Creating directory"))
+
 
       /* actual sources: with SHA1 digest */
 
@@ -322,6 +324,8 @@
       isabelle_logo.foreach(_.write(doc_dir))
       session_graph.write(doc_dir)
 
+      progress.bash("ls -alR", echo = true, cwd = doc_dir.file).check
+
       Directory(doc_dir, doc, root_name, sources)
     }
 
@@ -348,7 +352,7 @@
     ): String = {
       "if [ -f " + root_name_script(ext) + " ]\n" +
       "then\n" +
-      "  " + (if (title.nonEmpty) program_start_script(title) else "") +
+      "  " + (if (title.nonEmpty) program_running_script(title) else "") +
         exe + " " + root_name_script() + "\n" +
       (if (after.isEmpty) "" else "  " + after) +
       "fi\n"
@@ -393,9 +397,9 @@
       context.prepare_directory(dir, doc, new Latex.Output(context.options))
 
     def use_pdflatex: Boolean = false
-    def start_latex: String = program_start_script(if (use_pdflatex) "pdflatex" else "lualatex")
+    def running_latex: String = program_running_script(if (use_pdflatex) "pdflatex" else "lualatex")
     def latex_script(context: Context, directory: Directory): String =
-      start_latex + (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 = {
diff -r f1063cdb0093 -r 1eb55d6809b3 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Feb 01 20:57:15 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Feb 01 21:23:54 2023 +0100
@@ -105,7 +105,7 @@
 
   /* progress */
 
-  class Log_Progress extends Program_Progress(default_program = "build") {
+  class Log_Progress extends Program_Progress(default_title = "build") {
     progress =>
 
     override def detect_program(s: String): Option[String] =