# HG changeset patch
# User wenzelm
# Date 1314821407 -7200
# Node ID a3255c85327b39d52d0cb579ff965658f0c85783
# Parent  990ac978854c69e710a27ce5ed39e2ba97e1b9b6
crude display of node status;
tuned signature;

diff -r 990ac978854c -r a3255c85327b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 31 20:47:33 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 31 22:10:07 2011 +0200
@@ -359,6 +359,16 @@
       (change, copy(history = history + change))
     }
 
+    def command_state(version: Version, command: Command): Command.State =
+    {
+      require(is_assigned(version))
+      try {
+        the_exec(the_assignment(version).check_finished.command_execs
+          .getOrElse(command.id, fail))
+      }
+      catch { case _: State.Fail => command.empty_state }
+    }
+
 
     // persistent user-view
     def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
@@ -378,13 +388,7 @@
         val version = stable.version.get_finished
         val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
-
-        def command_state(command: Command): Command.State =
-          try {
-            the_exec(the_assignment(version).check_finished.command_execs
-              .getOrElse(command.id, fail))
-          }
-          catch { case _: State.Fail => command.empty_state }
+        def command_state(command: Command): Command.State = state.command_state(version, command)
 
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
diff -r 990ac978854c -r a3255c85327b src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Wed Aug 31 20:47:33 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Wed Aug 31 22:10:07 2011 +0200
@@ -33,8 +33,8 @@
   /* toplevel transactions */
 
   sealed abstract class Status
+  case object Unprocessed extends Status
   case class Forked(forks: Int) extends Status
-  case object Unprocessed extends Status
   case object Finished extends Status
   case object Failed extends Status
 
@@ -51,6 +51,25 @@
     else Unprocessed
   }
 
+  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
+
+  def node_status(
+    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
+  {
+    var unprocessed = 0
+    var running = 0
+    var finished = 0
+    var failed = 0
+    node.commands.foreach(command =>
+      command_status(state.command_state(version, command).status) match {
+        case Unprocessed => unprocessed += 1
+        case Forked(_) => running += 1
+        case Finished => finished += 1
+        case Failed => failed += 1
+      })
+    Node_Status(unprocessed, running, finished, failed)
+  }
+
 
   /* result messages */
 
diff -r 990ac978854c -r a3255c85327b src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 20:47:33 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 22:10:07 2011 +0200
@@ -73,15 +73,28 @@
 
   /* component state -- owned by Swing thread */
 
-  private var nodes: Set[String] = Set.empty
+  private var nodes_status: Map[String, String] = Map.empty
 
   private def handle_changed(changed_nodes: Set[String])
   {
     Swing_Thread.now {
-      val nodes1 = nodes ++ changed_nodes
-      if (nodes1 != nodes) {
-        nodes = nodes1
-        status.listData = Library.sort_strings(nodes.toList)
+      // FIXME correlation to changed_nodes!?
+      val state = Isabelle.session.current_state()
+      state.recent_stable.map(change => change.version.get_finished) match {
+        case None =>
+        case Some(version) =>
+          var nodes_status1 = nodes_status
+          for {
+            name <- changed_nodes
+            node <- version.nodes.get(name)
+            val status = Isar_Document.node_status(state, version, node)
+          } nodes_status1 += (name -> status.toString)
+
+          if (nodes_status != nodes_status1) {
+            nodes_status = nodes_status1
+            val order = Library.sort_strings(nodes_status.keySet.toList)
+            status.listData = order.map(name => name + " " + nodes_status(name))
+          }
       }
     }
   }