more visual emphasis on node status;
authorwenzelm
Fri, 25 Jun 2021 12:32:56 +0200
changeset 73872 ced6e3c03425
parent 73871 f46e9f75b7d5
child 73873 2d42e52152b1
more visual emphasis on node status;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/theories_dockable.scala
--- 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"
--- 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(