# HG changeset patch
# User wenzelm
# Date 1528573936 -7200
# Node ID 4e27f5c361d2674805b6a5f92cb891ea313048c9
# Parent  c8c3136e3ba7f43e0d6a3e16e43f7ac405656999
clarified signature: more uniform theory_message (see also d7920eb7de54);

diff -r c8c3136e3ba7 -r 4e27f5c361d2 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Jun 09 13:19:57 2018 +0200
+++ b/src/Pure/System/progress.scala	Sat Jun 09 21:52:16 2018 +0200
@@ -10,6 +10,12 @@
 import java.io.{File => JFile}
 
 
+object Progress
+{
+  def theory_message(session: String, theory: String): String =
+    if (session == "") "theory " + theory else session + ": theory " + theory
+}
+
 class Progress
 {
   def echo(msg: String) {}
@@ -51,10 +57,7 @@
   }
 
   override def theory(session: String, theory: String): Unit =
-    if (verbose) {
-      if (session == "") echo("theory " + theory)
-      else echo(session + ": theory " + theory)
-    }
+    if (verbose) echo(Progress.theory_message(session, theory))
 
   @volatile private var is_stopped = false
   override def interrupt_handler[A](e: => A): A =
@@ -72,7 +75,7 @@
     File.append(path, msg + "\n")
 
   override def theory(session: String, theory: String): Unit =
-    if (verbose) echo(session + ": theory " + theory)
+    if (verbose) echo(Progress.theory_message(session, theory))
 
   override def toString: String = path.toString
 }
diff -r c8c3136e3ba7 -r 4e27f5c361d2 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Jun 09 13:19:57 2018 +0200
+++ b/src/Pure/Tools/server.scala	Sat Jun 09 21:52:16 2018 +0200
@@ -269,7 +269,7 @@
     override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
     override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
     override def theory(session: String, theory: String): Unit =
-      context.writeln(session + ": theory " + theory,
+      context.writeln(Progress.theory_message(session, theory),
         (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
 
     @volatile private var is_stopped = false
diff -r c8c3136e3ba7 -r 4e27f5c361d2 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Sat Jun 09 13:19:57 2018 +0200
+++ b/src/Tools/VSCode/src/channel.scala	Sat Jun 09 21:52:16 2018 +0200
@@ -104,6 +104,6 @@
       override def echo_warning(msg: String): Unit = log_warning(msg)
       override def echo_error_message(msg: String): Unit = log_error_message(msg)
       override def theory(session: String, theory: String): Unit =
-        if (verbose) echo(session + ": theory " + theory)
+        if (verbose) echo(Progress.theory_message(session, theory))
     }
 }
diff -r c8c3136e3ba7 -r 4e27f5c361d2 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Jun 09 13:19:57 2018 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Jun 09 21:52:16 2018 +0200
@@ -68,7 +68,7 @@
         }
 
       override def theory(session: String, theory: String): Unit =
-        echo(session + ": theory " + theory)
+        echo(Progress.theory_message(session, theory))
 
       override def stopped: Boolean = is_stopped
     }