src/Tools/jEdit/src/rich_text_area.scala
changeset 51496 cb677987b7e3
parent 51492 eaa1c4cc1106
child 51574 2b58d7b139d6
     1.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 23 16:46:09 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 23 19:39:31 2013 +0100
     1.3 @@ -215,14 +215,16 @@
     1.4              JEdit_Lib.pixel_range(text_area, x, y) match {
     1.5                case None =>
     1.6                case Some(range) =>
     1.7 -                val tip =
     1.8 +                val result =
     1.9                    if (control) rendering.tooltip(range)
    1.10                    else rendering.tooltip_message(range)
    1.11 -                if (!tip.isEmpty) {
    1.12 -                  val painter = text_area.getPainter
    1.13 -                  val y1 = y + painter.getFontMetrics.getHeight / 2
    1.14 -                  val results = rendering.command_results(range)
    1.15 -                  Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
    1.16 +                result match {
    1.17 +                  case None =>
    1.18 +                  case Some(tip) =>
    1.19 +                    val painter = text_area.getPainter
    1.20 +                    val y1 = y + painter.getFontMetrics.getHeight / 2
    1.21 +                    val results = rendering.command_results(range)
    1.22 +                    Pretty_Tooltip(view, painter, rendering, x, y1, results, tip.range, tip.info)
    1.23                  }
    1.24              }
    1.25            }