1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 31 20:47:33 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 31 22:10:07 2011 +0200
     1.3 @@ -359,6 +359,16 @@
     1.4        (change, copy(history = history + change))
     1.5      }
     1.6  
     1.7 +    def command_state(version: Version, command: Command): Command.State =
     1.8 +    {
     1.9 +      require(is_assigned(version))
    1.10 +      try {
    1.11 +        the_exec(the_assignment(version).check_finished.command_execs
    1.12 +          .getOrElse(command.id, fail))
    1.13 +      }
    1.14 +      catch { case _: State.Fail => command.empty_state }
    1.15 +    }
    1.16 +
    1.17  
    1.18      // persistent user-view
    1.19      def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
    1.20 @@ -378,13 +388,7 @@
    1.21          val version = stable.version.get_finished
    1.22          val node = version.nodes(name)
    1.23          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.24 -
    1.25 -        def command_state(command: Command): Command.State =
    1.26 -          try {
    1.27 -            the_exec(the_assignment(version).check_finished.command_execs
    1.28 -              .getOrElse(command.id, fail))
    1.29 -          }
    1.30 -          catch { case _: State.Fail => command.empty_state }
    1.31 +        def command_state(command: Command): Command.State = state.command_state(version, command)
    1.32  
    1.33          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.34          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))

     2.1 --- a/src/Pure/PIDE/isar_document.scala	Wed Aug 31 20:47:33 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.scala	Wed Aug 31 22:10:07 2011 +0200
     2.3 @@ -33,8 +33,8 @@
     2.4    /* toplevel transactions */
     2.5  
     2.6    sealed abstract class Status
     2.7 +  case object Unprocessed extends Status
     2.8    case class Forked(forks: Int) extends Status
     2.9 -  case object Unprocessed extends Status
    2.10    case object Finished extends Status
    2.11    case object Failed extends Status
    2.12  
    2.13 @@ -51,6 +51,25 @@
    2.14      else Unprocessed
    2.15    }
    2.16  
    2.17 +  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
    2.18 +
    2.19 +  def node_status(
    2.20 +    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
    2.21 +  {
    2.22 +    var unprocessed = 0
    2.23 +    var running = 0
    2.24 +    var finished = 0
    2.25 +    var failed = 0
    2.26 +    node.commands.foreach(command =>
    2.27 +      command_status(state.command_state(version, command).status) match {
    2.28 +        case Unprocessed => unprocessed += 1
    2.29 +        case Forked(_) => running += 1
    2.30 +        case Finished => finished += 1
    2.31 +        case Failed => failed += 1
    2.32 +      })
    2.33 +    Node_Status(unprocessed, running, finished, failed)
    2.34 +  }
    2.35 +
    2.36  
    2.37    /* result messages */
    2.38  

     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 20:47:33 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 22:10:07 2011 +0200
     3.3 @@ -73,15 +73,28 @@
     3.4  
     3.5    /* component state -- owned by Swing thread */
     3.6  
     3.7 -  private var nodes: Set[String] = Set.empty
     3.8 +  private var nodes_status: Map[String, String] = Map.empty
     3.9  
    3.10    private def handle_changed(changed_nodes: Set[String])
    3.11    {
    3.12      Swing_Thread.now {
    3.13 -      val nodes1 = nodes ++ changed_nodes
    3.14 -      if (nodes1 != nodes) {
    3.15 -        nodes = nodes1
    3.16 -        status.listData = Library.sort_strings(nodes.toList)
    3.17 +      // FIXME correlation to changed_nodes!?
    3.18 +      val state = Isabelle.session.current_state()
    3.19 +      state.recent_stable.map(change => change.version.get_finished) match {
    3.20 +        case None =>
    3.21 +        case Some(version) =>
    3.22 +          var nodes_status1 = nodes_status
    3.23 +          for {
    3.24 +            name <- changed_nodes
    3.25 +            node <- version.nodes.get(name)
    3.26 +            val status = Isar_Document.node_status(state, version, node)
    3.27 +          } nodes_status1 += (name -> status.toString)
    3.28 +
    3.29 +          if (nodes_status != nodes_status1) {
    3.30 +            nodes_status = nodes_status1
    3.31 +            val order = Library.sort_strings(nodes_status.keySet.toList)
    3.32 +            status.listData = order.map(name => name + " " + nodes_status(name))
    3.33 +          }
    3.34        }
    3.35      }
    3.36    }