--- 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(