# HG changeset patch
# User wenzelm
# Date 1502703007 -7200
# Node ID 72a7e29104f1bc9ebe13029989479da5a0476115
# Parent  f749d39c016ba9bc48e54b7e5537441fb97a7244
explicit indication of consolidated nodes;

diff -r f749d39c016b -r 72a7e29104f1 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Aug 13 23:45:45 2017 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Aug 14 11:30:07 2017 +0200
@@ -126,13 +126,16 @@
   /* node status */
 
   sealed case class Node_Status(
-    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int)
+    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
   {
     def total: Int = unprocessed + running + warned + failed + finished
   }
 
   def node_status(
-    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
+    state: Document.State,
+    version: Document.Version,
+    name: Document.Node.Name,
+    node: Document.Node): Node_Status =
   {
     var unprocessed = 0
     var running = 0
@@ -149,7 +152,9 @@
       else if (status.is_finished) finished += 1
       else unprocessed += 1
     }
-    Node_Status(unprocessed, running, warned, failed, finished)
+    val consolidated = state.node_consolidated(version, name)
+
+    Node_Status(unprocessed, running, warned, failed, finished, consolidated)
   }
 
 
diff -r f749d39c016b -r 72a7e29104f1 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Aug 13 23:45:45 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 11:30:07 2017 +0200
@@ -95,6 +95,12 @@
   private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
   private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
 
+  private def nodes_status_consolidated(name: Document.Node.Name): Boolean =
+    nodes_status.get(name) match {
+      case None => false
+      case Some(st) => st.consolidated
+    }
+
   private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
     geometry match {
       case Some((loc, size)) =>
@@ -132,10 +138,6 @@
     val label = new Label {
       background = view.getTextArea.getPainter.getBackground
       foreground = view.getTextArea.getPainter.getForeground
-      border =
-        BorderFactory.createCompoundBorder(
-          BorderFactory.createLineBorder(foreground, 1),
-          BorderFactory.createEmptyBorder(1, 1, 1, 1))
       opaque = false
       xAlignment = Alignment.Leading
 
@@ -174,6 +176,15 @@
       }
     }
 
+    def label_border(name: Document.Node.Name)
+    {
+      label.border =
+        BorderFactory.createCompoundBorder(
+          BorderFactory.createLineBorder(
+            label.foreground, if (nodes_status_consolidated(name)) 3 else 1),
+          BorderFactory.createEmptyBorder(3, 3, 3, 3))
+    }
+
     layout(checkbox) = BorderPanel.Position.West
     layout(label) = BorderPanel.Position.Center
   }
@@ -186,6 +197,7 @@
       val component = Node_Renderer_Component
       component.node_name = name
       component.checkbox.selected = nodes_required.contains(name)
+      component.label_border(name)
       component.label.text = name.theory_base_name
       component
     }
@@ -208,7 +220,11 @@
       (nodes_status /: iterator)({ case (status, (name, node)) =>
           if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty)
             status
-          else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
+          else {
+            val st = Protocol.node_status(snapshot.state, snapshot.version, name, node)
+            status + (name -> st)
+          }
+      })
 
     val nodes_status2 =
       nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))