# HG changeset patch
# User wenzelm
# Date 1624617176 -7200
# Node ID ced6e3c0342563703007a654e8ab629952d57a77
# Parent  f46e9f75b7d5bb117bded29c3c27634066008da2
more visual emphasis on node status;

diff -r f46e9f75b7d5 -r ced6e3c03425 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Jun 24 06:06:32 2021 +0000
+++ b/src/Tools/jEdit/etc/options	Fri Jun 25 12:32:56 2021 +0200
@@ -99,6 +99,8 @@
 option warning_color : string = "FF8C00FF"
 option legacy_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
+option ok_color : string = "000000FF"
+option failed_color : string = "B22222FF"
 option writeln_message_color : string = "F0F0F0FF"
 option information_message_color : string = "DCEAF3FF"
 option tracing_message_color : string = "F0F8FFFF"
diff -r f46e9f75b7d5 -r ced6e3c03425 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Thu Jun 24 06:06:32 2021 +0000
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Jun 25 12:32:56 2021 +0200
@@ -180,11 +180,15 @@
     {
       val st = nodes_status.overall_node_status(name)
       val color =
-        if (st == Document_Status.Overall_Node_Status.failed)
-          PIDE.options.color_value("error_color")
-        else label.foreground
-      val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 2
-      val thickness2 = 3 - thickness1
+        st match {
+          case Document_Status.Overall_Node_Status.ok =>
+            PIDE.options.color_value("ok_color")
+          case Document_Status.Overall_Node_Status.failed =>
+            PIDE.options.color_value("failed_color")
+          case _ => label.foreground
+        }
+      val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
+      val thickness2 = 4 - thickness1
 
       label.border =
         BorderFactory.createCompoundBorder(