# HG changeset patch
# User wenzelm
# Date 1502719404 -7200
# Node ID 410b10ea405c041b20cd45e878f7a53f2045c6c5
# Parent  1f46b6693b56b8f2dc07712ff762a8c717154f1e
tuned GUI;

diff -r 1f46b6693b56 -r 410b10ea405c src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 15:52:07 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 16:03:24 2017 +0200
@@ -47,10 +47,14 @@
         val index_location = peer.indexToLocation(index)
         if (index >= 0 && in_checkbox(index_location, point))
           tooltip = "Mark as required for continuous checking"
-        else if (index >= 0 && in_label(index_location, point))
-          tooltip = "theory " + quote(listData(index).theory)
-        else
-          tooltip = null
+        else if (index >= 0 && in_label(index_location, point)) {
+          val name = listData(index)
+          val st = overall_node_status(name)
+          tooltip =
+            "theory " + quote(name.theory) +
+              (if (st == Overall_Node_Status.ok) "" else " (" + st + ")")
+        }
+        else tooltip = null
     }
   }
   status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)