clarified signature: more uniform theory_message (see also d7920eb7de54);
authorwenzelm
Sat Jun 09 21:52:16 2018 +0200 (11 months ago)
changeset 684104e27f5c361d2
parent 68409 c8c3136e3ba7
child 68411 d8363de26567
child 68420 529d6b132c27
clarified signature: more uniform theory_message (see also d7920eb7de54);
src/Pure/System/progress.scala
src/Pure/Tools/server.scala
src/Tools/VSCode/src/channel.scala
src/Tools/jEdit/src/session_build.scala
     1.1 --- a/src/Pure/System/progress.scala	Sat Jun 09 13:19:57 2018 +0200
     1.2 +++ b/src/Pure/System/progress.scala	Sat Jun 09 21:52:16 2018 +0200
     1.3 @@ -10,6 +10,12 @@
     1.4  import java.io.{File => JFile}
     1.5  
     1.6  
     1.7 +object Progress
     1.8 +{
     1.9 +  def theory_message(session: String, theory: String): String =
    1.10 +    if (session == "") "theory " + theory else session + ": theory " + theory
    1.11 +}
    1.12 +
    1.13  class Progress
    1.14  {
    1.15    def echo(msg: String) {}
    1.16 @@ -51,10 +57,7 @@
    1.17    }
    1.18  
    1.19    override def theory(session: String, theory: String): Unit =
    1.20 -    if (verbose) {
    1.21 -      if (session == "") echo("theory " + theory)
    1.22 -      else echo(session + ": theory " + theory)
    1.23 -    }
    1.24 +    if (verbose) echo(Progress.theory_message(session, theory))
    1.25  
    1.26    @volatile private var is_stopped = false
    1.27    override def interrupt_handler[A](e: => A): A =
    1.28 @@ -72,7 +75,7 @@
    1.29      File.append(path, msg + "\n")
    1.30  
    1.31    override def theory(session: String, theory: String): Unit =
    1.32 -    if (verbose) echo(session + ": theory " + theory)
    1.33 +    if (verbose) echo(Progress.theory_message(session, theory))
    1.34  
    1.35    override def toString: String = path.toString
    1.36  }
     2.1 --- a/src/Pure/Tools/server.scala	Sat Jun 09 13:19:57 2018 +0200
     2.2 +++ b/src/Pure/Tools/server.scala	Sat Jun 09 21:52:16 2018 +0200
     2.3 @@ -269,7 +269,7 @@
     2.4      override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
     2.5      override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
     2.6      override def theory(session: String, theory: String): Unit =
     2.7 -      context.writeln(session + ": theory " + theory,
     2.8 +      context.writeln(Progress.theory_message(session, theory),
     2.9          (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
    2.10  
    2.11      @volatile private var is_stopped = false
     3.1 --- a/src/Tools/VSCode/src/channel.scala	Sat Jun 09 13:19:57 2018 +0200
     3.2 +++ b/src/Tools/VSCode/src/channel.scala	Sat Jun 09 21:52:16 2018 +0200
     3.3 @@ -104,6 +104,6 @@
     3.4        override def echo_warning(msg: String): Unit = log_warning(msg)
     3.5        override def echo_error_message(msg: String): Unit = log_error_message(msg)
     3.6        override def theory(session: String, theory: String): Unit =
     3.7 -        if (verbose) echo(session + ": theory " + theory)
     3.8 +        if (verbose) echo(Progress.theory_message(session, theory))
     3.9      }
    3.10  }
     4.1 --- a/src/Tools/jEdit/src/session_build.scala	Sat Jun 09 13:19:57 2018 +0200
     4.2 +++ b/src/Tools/jEdit/src/session_build.scala	Sat Jun 09 21:52:16 2018 +0200
     4.3 @@ -68,7 +68,7 @@
     4.4          }
     4.5  
     4.6        override def theory(session: String, theory: String): Unit =
     4.7 -        echo(session + ": theory " + theory)
     4.8 +        echo(Progress.theory_message(session, theory))
     4.9  
    4.10        override def stopped: Boolean = is_stopped
    4.11      }