# HG changeset patch
# User wenzelm
# Date 1534597328 -7200
# Node ID 660944bf744a79c49638c099bd1db3fe21bfebe9
# Parent  8292cfd7b8193e8ce20104f7085a7b48cca038e3
tuned;

diff -r 8292cfd7b819 -r 660944bf744a src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 14:59:40 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 15:02:08 2018 +0200
@@ -177,12 +177,12 @@
 
     def label_border(name: Document.Node.Name)
     {
-      val status = nodes_status.overall_node_status(name)
+      val st = nodes_status.overall_node_status(name)
       val color =
-        if (status == Document_Status.Overall_Node_Status.failed)
+        if (st == Document_Status.Overall_Node_Status.failed)
           PIDE.options.color_value("error_color")
         else label.foreground
-      val thickness1 = if (status == Document_Status.Overall_Node_Status.pending) 1 else 2
+      val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 2
       val thickness2 = 3 - thickness1
 
       label.border =