--- a/src/Tools/jEdit/src/rendering.scala Wed Apr 02 11:55:37 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Wed Apr 02 12:26:11 2014 +0200
@@ -304,7 +304,7 @@
if (results.isEmpty) None
else {
val status =
- Protocol.command_status(results.iterator.flatMap(info => info.info._1.iterator))
+ Protocol.Status.make(results.iterator.flatMap(info => info.info._1.iterator))
val pri = (0 /: results.iterator.map(info => info.info._2))(_ max _)
if (status.is_running) Some(running_color)
@@ -628,7 +628,7 @@
color <-
(result match {
case (markups, opt_color) if !markups.isEmpty =>
- val status = Protocol.command_status(markups.iterator)
+ val status = Protocol.Status.make(markups.iterator)
if (status.is_unprocessed) Some(unprocessed1_color)
else if (status.is_running) Some(running1_color)
else opt_color