# HG changeset patch
# User wenzelm
# Date 1675190625 -3600
# Node ID 59a8b9a341aa1f05e826faa7cc4c4192357081a6
# Parent  c0633a0da53e1e6d51ab4672aad00509f29bae6c
proper program name, e.g. for session "Intro";

diff -r c0633a0da53e -r 59a8b9a341aa src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Jan 31 19:27:02 2023 +0100
+++ b/src/Pure/System/progress.scala	Tue Jan 31 19:43:45 2023 +0100
@@ -127,7 +127,7 @@
   }
 }
 
-abstract class Program_Progress extends Progress {
+abstract class Program_Progress(default_program: String = "program") extends Progress {
   private var _finished_programs: List[Program_Progress.Program] = Nil
   private var _running_program: Option[Program_Progress.Program] = None
 
@@ -161,7 +161,7 @@
         stop_program()
         start_program(title)
       case None =>
-        if (_running_program.isEmpty) start_program("program")
+        if (_running_program.isEmpty) start_program(default_program)
         _running_program.get.echo(msg)
     }
   }
diff -r c0633a0da53e -r 59a8b9a341aa src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 19:27:02 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 19:43:45 2023 +0100
@@ -105,7 +105,7 @@
 
   /* progress */
 
-  class Log_Progress extends Program_Progress {
+  class Log_Progress extends Program_Progress(default_program = "build") {
     progress =>
 
     override def detect_program(s: String): Option[String] =