# HG changeset patch
# User wenzelm
# Date 1550502790 -3600
# Node ID dfc5f8294fbc3e279c5cc9513eb790ed09db45c6
# Parent  32c4f01a5e339919d3d8cb5385ab0e11b3408d6a
suppress nodes with vacuous status, notably empty nodes (amending 5f160df596c1);

diff -r 32c4f01a5e33 -r dfc5f8294fbc src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Feb 18 16:04:52 2019 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Feb 18 16:13:10 2019 +0100
@@ -150,7 +150,7 @@
 
         paint_segment(0, size.width, background)
         nodes_status.get(node_name) match {
-          case Some(node_status) if node_status.total > 0 =>
+          case Some(node_status) =>
             val segments =
               List(
                 (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")),
@@ -165,7 +165,7 @@
               last - w - 1
             })
 
-          case _ =>
+          case None =>
             paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
         }
         super.paintComponent(gfx)
@@ -223,8 +223,10 @@
     nodes_status = nodes_status1
     if (nodes_status_changed) {
       status.listData =
-        (for { (name, node_status) <- nodes_status1.present.iterator if !node_status.is_suppressed }
-          yield name).toList
+        (for {
+          (name, node_status) <- nodes_status1.present.iterator
+          if !node_status.is_suppressed && node_status.total > 0
+        } yield name).toList
     }
   }