# HG changeset patch
# User wenzelm
# Date 1536831699 -7200
# Node ID e86d6e869b965fd1ebcf473ee8dc2328a214840d
# Parent  22f02724e7d1d449f7d596eab51814c694a87b64
tuned signature;

diff -r 22f02724e7d1 -r e86d6e869b96 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu Sep 13 11:24:24 2018 +0200
+++ b/src/Pure/System/progress.scala	Thu Sep 13 11:41:39 2018 +0200
@@ -14,9 +14,12 @@
 {
   sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None)
   {
-    def message: String =
-      (if (session == "") "theory " + theory else session + ": theory " + theory) +
-      (percentage match { case None => "" case Some(p) => " " + p + "%" })
+    def message: String = print_session + print_theory + print_percentage
+
+    def print_session: String = if (session == "") "" else session + ": "
+    def print_theory: String = "theory " + theory
+    def print_percentage: String =
+      percentage match { case None => "" case Some(p) => " " + p + "%" }
   }
 }