# HG changeset patch
# User wenzelm
# Date 1496861163 -7200
# Node ID fd8a65b026f17dd85bf603e324021d03eda0ef68
# Parent  94cfcae2b228dbf275753f3fc1a26b20c4a89181
more tooltips;

diff -r 94cfcae2b228 -r fd8a65b026f1 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jun 07 20:18:23 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jun 07 20:46:03 2017 +0200
@@ -44,8 +44,11 @@
         }
       case MouseMoved(_, point, _) =>
         val index = peer.locationToIndex(point)
-        if (index >= 0 && in_checkbox(peer.indexToLocation(index), point))
+        val index_location = peer.indexToLocation(index)
+        if (index >= 0 && in_checkbox(index_location, point))
           tooltip = "Mark as required for continuous checking"
+        if (index >= 0 && in_label(index_location, point))
+          tooltip = "theory " + quote(listData(index).theory)
         else
           tooltip = null
     }
@@ -91,14 +94,20 @@
   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 in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
+    geometry match {
+      case Some((loc, size)) =>
+        loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
+        loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
+      case None => false
+    }
+
   private def in_checkbox(loc0: Point, p: Point): Boolean =
-    Node_Renderer_Component != null &&
-      (Node_Renderer_Component.checkbox_geometry match {
-        case Some((loc, size)) =>
-          loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
-          loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
-        case None => false
-      })
+    Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p)
+
+  private def in_label(loc0: Point, p: Point): Boolean =
+    Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p)
+
 
   private object Node_Renderer_Component extends BorderPanel
   {
@@ -118,6 +127,7 @@
       }
     }
 
+    var label_geometry: Option[(Point, Dimension)] = None
     val label = new Label {
       background = view.getTextArea.getPainter.getBackground
       foreground = view.getTextArea.getPainter.getForeground
@@ -157,6 +167,9 @@
             paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
         }
         super.paintComponent(gfx)
+
+        if (location != null && size != null)
+          label_geometry = Some((location, size))
       }
     }