--- 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 + "%" }
}
}