tuned;
authorwenzelm
Sat, 18 Aug 2018 15:02:08 +0200
changeset 68768 660944bf744a
parent 68767 8292cfd7b819
child 68769 59fcff4f8b73
tuned;
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 =