# HG changeset patch
# User wenzelm
# Date 1396434371 -7200
# Node ID bca016a9a18d9b66dee64064c35b9dc2890f934f
# Parent  ed09e5f3aedfe68e1c5e1a40112ec99f4d89a556
persistent protocol_status, to improve performance of node_status a little;

diff -r ed09e5f3aedf -r bca016a9a18d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Apr 02 11:55:37 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Apr 02 12:26:11 2014 +0200
@@ -109,13 +109,11 @@
     results: Results = Results.empty,
     markups: Markups = Markups.empty)
   {
-    /* markup */
+    lazy val protocol_status: Protocol.Status = Protocol.Status.make(status.iterator)
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 
 
-    /* content */
-
     def eq_content(other: State): Boolean =
       command.source == other.command.source &&
       status == other.status &&
diff -r ed09e5f3aedf -r bca016a9a18d src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Apr 02 11:55:37 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Apr 02 12:26:11 2014 +0200
@@ -41,6 +41,39 @@
 
   /* command status */
 
+  object Status
+  {
+    def make(markup_iterator: Iterator[Markup]): Status =
+    {
+      var touched = false
+      var accepted = false
+      var failed = false
+      var forks = 0
+      var runs = 0
+      for (markup <- markup_iterator) {
+        markup.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 empty = make(Iterator.empty)
+
+    def merge(status_iterator: Iterator[Status]): Status =
+      if (status_iterator.hasNext) {
+        val status0 = status_iterator.next
+        (status0 /: status_iterator)(_ + _)
+      }
+      else empty
+  }
+
   sealed case class Status(
     private val touched: Boolean,
     private val accepted: Boolean,
@@ -48,33 +81,16 @@
     forks: Int,
     runs: Int)
   {
+    def + (that: Status): Status =
+      Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
+        forks + that.forks, runs + that.runs)
+
     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
     def is_running: Boolean = runs != 0
     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
     def is_failed: Boolean = failed
   }
 
-  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) {
-      markup.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,
       Markup.FINISHED, Markup.FAILED)
@@ -117,7 +133,7 @@
     var failed = 0
     for (command <- node.commands.iterator) {
       val states = state.command_states(version, command)
-      val status = command_status(states.iterator.flatMap(st => st.status.iterator))
+      val status = Status.merge(states.iterator.map(_.protocol_status))
 
       if (status.is_running) running += 1
       else if (status.is_finished) {
diff -r ed09e5f3aedf -r bca016a9a18d src/Tools/jEdit/src/rendering.scala
--- 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