# HG changeset patch
# User wenzelm
# Date 1550502292 -3600
# Node ID 32c4f01a5e339919d3d8cb5385ab0e11b3408d6a
# Parent  60d0ee8f2ddb93777845226d176ad3cef6c79908
tuned;

diff -r 60d0ee8f2ddb -r 32c4f01a5e33 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Feb 18 15:57:06 2019 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Feb 18 16:04:52 2019 +0100
@@ -150,17 +150,17 @@
 
         paint_segment(0, size.width, background)
         nodes_status.get(node_name) match {
-          case Some(st) if st.total > 0 =>
+          case Some(node_status) if node_status.total > 0 =>
             val segments =
               List(
-                (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
-                (st.running, PIDE.options.color_value("running_color")),
-                (st.warned, PIDE.options.color_value("warning_color")),
-                (st.failed, PIDE.options.color_value("error_color"))
+                (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")),
+                (node_status.running, PIDE.options.color_value("running_color")),
+                (node_status.warned, PIDE.options.color_value("warning_color")),
+                (node_status.failed, PIDE.options.color_value("error_color"))
               ).filter(_._1 > 0)
 
             ((size.width - 2) /: segments)({ case (last, (n, color)) =>
-              val w = (n * ((size.width - 4) - segments.length) / st.total) max 4
+              val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
               paint_segment(last - w, w, color)
               last - w - 1
             })