# HG changeset patch
# User wenzelm
# Date 1502711629 -7200
# Node ID 72de7d59e2f7b4a7e8064539422b8c38cea67d36
# Parent  72a7e29104f1bc9ebe13029989479da5a0476115
more explicit failure;

diff -r 72a7e29104f1 -r 72de7d59e2f7 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Aug 14 11:30:07 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Aug 14 13:53:49 2017 +0200
@@ -129,6 +129,7 @@
     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
   {
     def total: Int = unprocessed + running + warned + failed + finished
+    def ok: Boolean = failed == 0
   }
 
   def node_status(
diff -r 72a7e29104f1 -r 72de7d59e2f7 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 11:30:07 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 13:53:49 2017 +0200
@@ -95,10 +95,16 @@
   private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
   private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
 
-  private def nodes_status_consolidated(name: Document.Node.Name): Boolean =
+  private object Overall_Node_Status extends Enumeration
+  {
+    val ok, failed, pending = Value
+  }
+
+  private def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
     nodes_status.get(name) match {
-      case None => false
-      case Some(st) => st.consolidated
+      case Some(st) if st.consolidated =>
+        if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
+      case _ => Overall_Node_Status.pending
     }
 
   private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
@@ -178,10 +184,15 @@
 
     def label_border(name: Document.Node.Name)
     {
+      val status = overall_node_status(name)
+      val color =
+        if (status == Overall_Node_Status.failed) PIDE.options.color_value("error_color")
+        else label.foreground
+      val thickness = if (status == Overall_Node_Status.pending) 1 else 3
+
       label.border =
         BorderFactory.createCompoundBorder(
-          BorderFactory.createLineBorder(
-            label.foreground, if (nodes_status_consolidated(name)) 3 else 1),
+          BorderFactory.createLineBorder(color, thickness),
           BorderFactory.createEmptyBorder(3, 3, 3, 3))
     }