clarified modules;

--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 12:41:05 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:33:40 2018 +0200
@@ -156,4 +156,46 @@
   }
 
   sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
+
+
+  /* nodes status */
+
+  object Overall_Node_Status extends Enumeration
+  {
+    val ok, failed, pending = Value
+  }
+
+  object Nodes_Status
+  {
+    val empty: Nodes_Status = new Nodes_Status(Map.empty)
+  }
+
+  final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
+  {
+    def keys_iterator: Iterator[Document.Node.Name] = rep.keysIterator
+
+    def defined(name: Document.Node.Name): Boolean = rep.isDefinedAt(name)
+    def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
+
+    def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
+      rep.get(name) match {
+        case Some(st) if st.consolidated =>
+          if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
+        case _ => Overall_Node_Status.pending
+      }
+
+    def + (entry: (Document.Node.Name, Node_Status)): Nodes_Status =
+      new Nodes_Status(rep + entry)
+
+    def - (name: Document.Node.Name): Nodes_Status =
+      new Nodes_Status(rep - name)
+
+    override def hashCode: Int = rep.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Nodes_Status => rep == other.rep
+        case _ => false
+      }
+    override def toString: String = rep.iterator.mkString("Nodes_Status(", ", ", ")")
+  }
 }

--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 12:41:05 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 13:33:40 2018 +0200
@@ -50,10 +50,10 @@
           tooltip = "Mark as required for continuous checking"
         else if (index >= 0 && in_label(index_location, point)) {
           val name = listData(index)
-          val st = overall_node_status(name)
+          val st = nodes_status.overall_node_status(name)
           tooltip =
             "theory " + quote(name.theory) +
-              (if (st == Overall_Node_Status.ok) "" else " (" + st + ")")
+              (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")")
         }
         else tooltip = null
     }
@@ -97,21 +97,9 @@
 
   /* component state -- owned by GUI thread */
 
-  private var nodes_status: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty
+  private var nodes_status = Document_Status.Nodes_Status.empty
   private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
 
-  private object Overall_Node_Status extends Enumeration
-  {
-    val ok, failed, pending = Value
-  }
-
-  private def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
-    nodes_status.get(name) match {
-      case Some(st) if st.consolidated =>
-        if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
-      case _ => Overall_Node_Status.pending
-    }
-
   private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
     geometry match {
       case Some((loc, size)) =>
@@ -189,11 +177,12 @@
 
     def label_border(name: Document.Node.Name)
     {
-      val status = overall_node_status(name)
+      val status = nodes_status.overall_node_status(name)
       val color =
-        if (status == Overall_Node_Status.failed) PIDE.options.color_value("error_color")
+        if (status == Document_Status.Overall_Node_Status.failed)
+          PIDE.options.color_value("error_color")
         else label.foreground
-      val thickness1 = if (status == Overall_Node_Status.pending) 1 else 2
+      val thickness1 = if (status == Document_Status.Overall_Node_Status.pending) 1 else 2
       val thickness2 = 3 - thickness1
 
       label.border =
@@ -241,11 +230,11 @@
         })
 
     val nodes_status2 =
-      nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_suppressed(_))
+      (nodes_status1 /: nodes_status1.keys_iterator.filter(nodes.is_suppressed(_)))(_ - _)
 
     if (nodes_status != nodes_status2) {
       nodes_status = nodes_status2
-      status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_))
+      status.listData = nodes.topological_order.filter(nodes_status.defined(_))
     }
   }