# HG changeset patch
# User wenzelm
# Date 1375300169 -7200
# Node ID 408fb2e563df2cdb0cb6583f750be3cda6edb985
# Parent  c608e0ade554388765e89201bea301145ee479e2
added home-made tooltips;
tuned signature;

diff -r c608e0ade554 -r 408fb2e563df src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 21:13:05 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 21:49:29 2013 +0200
@@ -12,7 +12,7 @@
 import scala.actors.Actor._
 import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
   ScrollPane, Component, CheckBox, BorderPanel}
-import scala.swing.event.{ButtonClicked, MouseClicked}
+import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
 
 import java.lang.System
 import java.awt.{BorderLayout, Graphics2D, Insets, Point, Dimension}
@@ -28,30 +28,27 @@
 
   private val status = new ListView(Nil: List[Document.Node.Name]) {
     listenTo(mouse.clicks)
+    listenTo(mouse.moves)
     reactions += {
       case MouseClicked(_, point, _, clicks, _) =>
         val index = peer.locationToIndex(point)
-        if (index >= 0 && Node_Renderer_Component != null) {
-          Node_Renderer_Component.checkbox_geometry match {
-            case Some((loc, size)) =>
-              val loc0 = peer.indexToLocation(index)
-              val in_checkbox =
-                loc0.x + loc.x <= point.x && point.x < loc0.x + size.width &&
-                loc0.y + loc.y <= point.y && point.y < loc0.y + size.height
-
-              if (clicks == 1 && in_checkbox) {
-                for {
-                  buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
-                  model <- PIDE.document_model(buffer)
-                } model.node_required = !model.node_required
-              }
-
-              if (clicks == 2 && !in_checkbox)
-                Hyperlink(listData(index).node).follow(view)
-
-            case None =>
+        if (index >= 0) {
+          if (in_checkbox(peer.indexToLocation(index), point)) {
+            if (clicks == 1) {
+              for {
+                buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
+                model <- PIDE.document_model(buffer)
+              } model.node_required = !model.node_required
+            }
           }
+          else if (clicks == 2) Hyperlink(listData(index).node).follow(view)
         }
+      case MouseMoved(_, point, _) =>
+        val index = peer.locationToIndex(point)
+        if (index >= 0 && in_checkbox(peer.indexToLocation(index), point))
+          tooltip = "Mark as required for continuous checking"
+        else
+          tooltip = null
     }
   }
   status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
@@ -104,6 +101,15 @@
     } nodes_required += model.name
   }
 
+  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
+      })
+
   private object Node_Renderer_Component extends BorderPanel
   {
     opaque = false