more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
authorwenzelm
Fri Oct 19 21:52:45 2012 +0200 (2012-10-19)
changeset 49941f2db0596bd61
parent 49940 d5f143b96334
child 49942 50e457bbc5fe
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 19 21:19:06 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 19 21:52:45 2012 +0200
     1.3 @@ -168,5 +168,17 @@
     1.4        Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
     1.5      else None
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* pixel range */
    1.10 +
    1.11 +  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
    1.12 +  {
    1.13 +    val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y))
    1.14 +    gfx_range(text_area, range) match {
    1.15 +      case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
    1.16 +      case _ => None
    1.17 +    }
    1.18 +  }
    1.19  }
    1.20  
     2.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 19 21:19:06 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 19 21:52:45 2012 +0200
     2.3 @@ -173,14 +173,16 @@
     2.4  
     2.5          if ((control || hovering) && !buffer.isLoading) {
     2.6            JEdit_Lib.buffer_lock(buffer) {
     2.7 -            val rendering = get_rendering()
     2.8 -            val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
     2.9 -            val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
    2.10 -            for ((area, require_control) <- active_areas)
    2.11 -            {
    2.12 -              if (control == require_control)
    2.13 -                area.update_rendering(rendering, mouse_range)
    2.14 -              else area.reset
    2.15 +            JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
    2.16 +              case None =>
    2.17 +              case Some(range) =>
    2.18 +                val rendering = get_rendering()
    2.19 +                for ((area, require_control) <- active_areas)
    2.20 +                {
    2.21 +                  if (control == require_control)
    2.22 +                    area.update_rendering(rendering, range)
    2.23 +                  else area.reset
    2.24 +                }
    2.25              }
    2.26            }
    2.27          }
    2.28 @@ -200,15 +202,17 @@
    2.29          val rendering = get_rendering()
    2.30          val snapshot = rendering.snapshot
    2.31          if (!snapshot.is_outdated) {
    2.32 -          val offset = text_area.xyToOffset(x, y)
    2.33 -          val range = Text.Range(offset, offset + 1)
    2.34 -          val tip =
    2.35 -            if (control) rendering.tooltip(range)
    2.36 -            else rendering.tooltip_message(range)
    2.37 -          if (!tip.isEmpty) {
    2.38 -            val painter = text_area.getPainter
    2.39 -            val y1 = y + painter.getFontMetrics.getHeight / 2
    2.40 -            new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
    2.41 +          JEdit_Lib.pixel_range(text_area, x, y) match {
    2.42 +            case None =>
    2.43 +            case Some(range) =>
    2.44 +              val tip =
    2.45 +                if (control) rendering.tooltip(range)
    2.46 +                else rendering.tooltip_message(range)
    2.47 +              if (!tip.isEmpty) {
    2.48 +                val painter = text_area.getPainter
    2.49 +                val y1 = y + painter.getFontMetrics.getHeight / 2
    2.50 +                new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
    2.51 +              }
    2.52            }
    2.53          }
    2.54          null