1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 18:06:34 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 18:14:54 2012 +0200
     1.3 @@ -107,5 +107,42 @@
     1.4        buffer.getLineOfOffset(range.start),
     1.5        buffer.getLineOfOffset(range.stop))
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* char width */
    1.10 +
    1.11 +  def char_width(text_area: TextArea): Int =
    1.12 +  {
    1.13 +    val painter = text_area.getPainter
    1.14 +    val font = painter.getFont
    1.15 +    val font_context = painter.getFontRenderContext
    1.16 +    font.getStringBounds(" ", font_context).getWidth.round.toInt
    1.17 +  }
    1.18 +
    1.19 +
    1.20 +  /* graphics range */
    1.21 +
    1.22 +  class Gfx_Range(val x: Int, val y: Int, val length: Int)
    1.23 +
    1.24 +  // NB: jEdit already normalizes \r\n and \r to \n
    1.25 +  // NB: last line lacks \n
    1.26 +  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    1.27 +  {
    1.28 +    val buffer = text_area.getBuffer
    1.29 +
    1.30 +    val p = text_area.offsetToXY(range.start)
    1.31 +
    1.32 +    val end = buffer.getLength
    1.33 +    val stop = range.stop
    1.34 +    val (q, r) =
    1.35 +      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area))
    1.36 +      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    1.37 +        (text_area.offsetToXY(stop - 1), char_width(text_area))
    1.38 +      else (text_area.offsetToXY(stop), 0)
    1.39 +
    1.40 +    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
    1.41 +      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
    1.42 +    else None
    1.43 +  }
    1.44  }
    1.45