--- 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
}
--- 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
--- 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))
}
}
--- 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
}