# HG changeset patch
# User wenzelm
# Date 1527616810 -7200
# Node ID daca5f2a0c9018cbb5d0d7881e6fe357e8eb3955
# Parent  1d33697199c1c215b273189adbaa49fcd91da0b4
tuned signature;

diff -r 1d33697199c1 -r daca5f2a0c90 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Tue May 29 18:09:08 2018 +0200
+++ b/src/Pure/General/graph.scala	Tue May 29 20:00:10 2018 +0200
@@ -66,6 +66,7 @@
 
   def is_empty: Boolean = rep.isEmpty
   def defined(x: Key): Boolean = rep.isDefinedAt(x)
+  def domain: Set[Key] = rep.keySet
 
   def iterator: Iterator[(Key, Entry)] = rep.iterator
 
diff -r 1d33697199c1 -r daca5f2a0c90 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue May 29 18:09:08 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue May 29 20:00:10 2018 +0200
@@ -383,6 +383,8 @@
       new Nodes(graph3.map_node(name, _ => node))
     }
 
+    def domain: Set[Node.Name] = graph.domain
+
     def iterator: Iterator[(Node.Name, Node)] =
       graph.iterator.map({ case (name, (node, _)) => (name, node) })
 
diff -r 1d33697199c1 -r daca5f2a0c90 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue May 29 18:09:08 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue May 29 20:00:10 2018 +0200
@@ -156,9 +156,10 @@
   def node_status(
     state: Document.State,
     version: Document.Version,
-    name: Document.Node.Name,
-    node: Document.Node): Node_Status =
+    name: Document.Node.Name): Node_Status =
   {
+    val node = version.nodes(name)
+
     var unprocessed = 0
     var running = 0
     var warned = 0
diff -r 1d33697199c1 -r daca5f2a0c90 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Tue May 29 18:09:08 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Tue May 29 20:00:10 2018 +0200
@@ -133,7 +133,7 @@
           case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
             val nodes =
               for (name <- dep_theories)
-              yield (name -> Protocol.node_status(state, version, name, version.nodes(name)))
+              yield (name -> Protocol.node_status(state, version, name))
             try { result.fulfill(Theories_Result(state, version, nodes)) }
             catch { case _: IllegalStateException => }
           case _ =>
diff -r 1d33697199c1 -r daca5f2a0c90 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue May 29 18:09:08 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue May 29 20:00:10 2018 +0200
@@ -228,21 +228,17 @@
     val snapshot = PIDE.session.snapshot()
     val nodes = snapshot.version.nodes
 
-    val iterator =
-      restriction match {
-        case Some(names) => names.iterator.map(name => (name, nodes(name)))
-        case None => nodes.iterator
-      }
     val nodes_status1 =
-      (nodes_status /: iterator)({ case (status, (name, node)) =>
-          if (PIDE.resources.is_hidden(name) ||
-              PIDE.resources.session_base.loaded_theory(name) ||
-              node.is_empty) status
-          else {
-            val st = Protocol.node_status(snapshot.state, snapshot.version, name, node)
-            status + (name -> st)
-          }
-      })
+      (nodes_status /: (restriction.getOrElse(nodes.domain).iterator))(
+        { case (status, name) =>
+            if (PIDE.resources.is_hidden(name) ||
+                PIDE.resources.session_base.loaded_theory(name) ||
+                nodes(name).is_empty) status
+            else {
+              val st = Protocol.node_status(snapshot.state, snapshot.version, name)
+              status + (name -> st)
+            }
+        })
 
     val nodes_status2 =
       nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_suppressed(_))