more tooltips;
authorwenzelm
Wed Jun 07 20:46:03 2017 +0200 (23 months ago)
changeset 66032fd8a65b026f1
parent 66031 94cfcae2b228
child 66033 e4a8e1e20d45
more tooltips;
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jun 07 20:18:23 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jun 07 20:46:03 2017 +0200
     1.3 @@ -44,8 +44,11 @@
     1.4          }
     1.5        case MouseMoved(_, point, _) =>
     1.6          val index = peer.locationToIndex(point)
     1.7 -        if (index >= 0 && in_checkbox(peer.indexToLocation(index), point))
     1.8 +        val index_location = peer.indexToLocation(index)
     1.9 +        if (index >= 0 && in_checkbox(index_location, point))
    1.10            tooltip = "Mark as required for continuous checking"
    1.11 +        if (index >= 0 && in_label(index_location, point))
    1.12 +          tooltip = "theory " + quote(listData(index).theory)
    1.13          else
    1.14            tooltip = null
    1.15      }
    1.16 @@ -91,14 +94,20 @@
    1.17    private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
    1.18    private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
    1.19  
    1.20 +  private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
    1.21 +    geometry match {
    1.22 +      case Some((loc, size)) =>
    1.23 +        loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
    1.24 +        loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
    1.25 +      case None => false
    1.26 +    }
    1.27 +
    1.28    private def in_checkbox(loc0: Point, p: Point): Boolean =
    1.29 -    Node_Renderer_Component != null &&
    1.30 -      (Node_Renderer_Component.checkbox_geometry match {
    1.31 -        case Some((loc, size)) =>
    1.32 -          loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
    1.33 -          loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
    1.34 -        case None => false
    1.35 -      })
    1.36 +    Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p)
    1.37 +
    1.38 +  private def in_label(loc0: Point, p: Point): Boolean =
    1.39 +    Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p)
    1.40 +
    1.41  
    1.42    private object Node_Renderer_Component extends BorderPanel
    1.43    {
    1.44 @@ -118,6 +127,7 @@
    1.45        }
    1.46      }
    1.47  
    1.48 +    var label_geometry: Option[(Point, Dimension)] = None
    1.49      val label = new Label {
    1.50        background = view.getTextArea.getPainter.getBackground
    1.51        foreground = view.getTextArea.getPainter.getForeground
    1.52 @@ -157,6 +167,9 @@
    1.53              paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
    1.54          }
    1.55          super.paintComponent(gfx)
    1.56 +
    1.57 +        if (location != null && size != null)
    1.58 +          label_geometry = Some((location, size))
    1.59        }
    1.60      }
    1.61