# 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 } }