tuned;
authorwenzelm
Mon, 18 Feb 2019 16:04:52 +0100
changeset 69819 32c4f01a5e33
parent 69818 60d0ee8f2ddb
child 69820 dfc5f8294fbc
tuned;
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
             })