# HG changeset patch
# User wenzelm
# Date 1396365992 -7200
# Node ID abdc524db8b42f41e67bd73c523f56bbd9fe725f
# Parent  1c735e46acf08f10ae823a29485880e851c6dc55
more frugal command_status, which is often used in a tight loop;

diff -r 1c735e46acf0 -r abdc524db8b4 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 01 16:16:25 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Apr 01 17:26:32 2014 +0200
@@ -41,17 +41,12 @@
 
   /* command status */
 
-  object Status
-  {
-    val init = Status()
-  }
-
   sealed case class Status(
-    private val touched: Boolean = false,
-    private val accepted: Boolean = false,
-    private val failed: Boolean = false,
-    forks: Int = 0,
-    runs: Int = 0)
+    private val touched: Boolean,
+    private val accepted: Boolean,
+    private val failed: Boolean,
+    forks: Int,
+    runs: Int)
   {
     def + (that: Status): Status =
       Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
@@ -63,22 +58,25 @@
     def is_failed: Boolean = failed
   }
 
-  def command_status(status: Status, markup: Markup): Status =
-    markup match {
-      case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
-      case Markup(Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
-      case Markup(Markup.JOINED, _) => status.copy(forks = status.forks - 1)
-      case Markup(Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
-      case Markup(Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
-      case Markup(Markup.FAILED, _) => status.copy(failed = true)
-      case _ => status
-    }
-
-  def command_status(status: Status, state: Command.State): Status =
-    (status /: state.status)(command_status(_, _))
-
-  def command_status(status: Status, states: List[Command.State]): Status =
-    (status /: states)(command_status(_, _))
+  def command_status(markups: Iterator[Markup]): Status =
+  {
+    var touched = false
+    var accepted = false
+    var failed = false
+    var forks = 0
+    var runs = 0
+    for { markup <- markups; name = markup.name }
+      name match {
+        case Markup.ACCEPTED => accepted = true
+        case Markup.FORKED => touched = true; forks += 1
+        case Markup.JOINED => forks -= 1
+        case Markup.RUNNING => touched = true; runs += 1
+        case Markup.FINISHED => runs -= 1
+        case Markup.FAILED => failed = true
+        case _ =>
+      }
+    Status(touched, accepted, failed, forks, runs)
+  }
 
   val command_status_elements =
     Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
@@ -123,7 +121,7 @@
     for {
       command <- node.commands
       states = state.command_states(version, command)
-      status = command_status(Status.init, states)
+      status = command_status(states.iterator.flatMap(st => st.status.iterator))
     } {
       if (status.is_running) running += 1
       else if (status.is_finished) {
diff -r 1c735e46acf0 -r abdc524db8b4 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue Apr 01 16:16:25 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Apr 01 17:26:32 2014 +0200
@@ -292,20 +292,20 @@
     if (snapshot.is_outdated) None
     else {
       val results =
-        snapshot.cumulate[(Protocol.Status, Int)](
-          range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
+        snapshot.cumulate[(List[Markup], Int)](
+          range, (Nil, 0), Protocol.status_elements, _ =>
           {
             case ((status, pri), Text.Info(_, elem)) =>
               if (Protocol.command_status_elements(elem.name))
-                Some((Protocol.command_status(status, elem.markup), pri))
+                Some((elem.markup :: status), pri)
               else
                 Some((status, pri max Rendering.message_pri(elem.name)))
           }, status = true)
       if (results.isEmpty) None
       else {
-        val (status, pri) =
-          ((Protocol.Status.init, 0) /: results) {
-            case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
+        val status =
+          Protocol.command_status(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)
         else if (pri == Rendering.warning_pri) Some(warning_color)
@@ -604,31 +604,32 @@
     else
       for {
         Text.Info(r, result) <-
-          snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
-            range, (Some(Protocol.Status.init), None), Rendering.background_elements,
+          snapshot.cumulate[(List[Markup], Option[Color])](
+            range, (List(Markup.Empty), None), Rendering.background_elements,
             command_results =>
               {
-                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
-                if (Protocol.command_status_elements(markup.name)) =>
-                  Some((Some(Protocol.command_status(status, markup)), color))
+                case (((status, color), Text.Info(_, XML.Elem(markup, _))))
+                if !status.isEmpty && Protocol.command_status_elements(markup.name) =>
+                  Some((markup :: status, color))
                 case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
-                  Some((None, Some(bad_color)))
+                  Some((Nil, Some(bad_color)))
                 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
-                  Some((None, Some(intensify_color)))
+                  Some((Nil, Some(intensify_color)))
                 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
                   command_results.get(serial) match {
                     case Some(Protocol.Dialog_Result(res)) if res == result =>
-                      Some((None, Some(active_result_color)))
+                      Some((Nil, Some(active_result_color)))
                     case _ =>
-                      Some((None, Some(active_color)))
+                      Some((Nil, Some(active_color)))
                   }
                 case (_, Text.Info(_, elem)) =>
-                  if (Rendering.active_elements(elem.name)) Some((None, Some(active_color)))
+                  if (Rendering.active_elements(elem.name)) Some((Nil, Some(active_color)))
                   else None
               })
         color <-
           (result match {
-            case (Some(status), opt_color) =>
+            case (markups, opt_color) if !markups.isEmpty =>
+              val status = Protocol.command_status(markups.iterator)
               if (status.is_unprocessed) Some(unprocessed1_color)
               else if (status.is_running) Some(running1_color)
               else opt_color