src/Tools/jEdit/src/jedit_lib.scala
changeset 50849 70f7483df9cb
parent 50658 0464c2007a25
child 51078 4e1c940b1fb2
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Jan 12 18:13:28 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Jan 12 19:53:24 2013 +0100
     1.3 @@ -160,17 +160,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* char width */
     1.8 -
     1.9 -  def char_width(text_area: TextArea): Int =
    1.10 -  {
    1.11 -    val painter = text_area.getPainter
    1.12 -    val font = painter.getFont
    1.13 -    val font_context = painter.getFontRenderContext
    1.14 -    font.getStringBounds(" ", font_context).getWidth.round.toInt
    1.15 -  }
    1.16 -
    1.17 -
    1.18    /* graphics range */
    1.19  
    1.20    case class Gfx_Range(val x: Int, val y: Int, val length: Int)
    1.21 @@ -179,6 +168,8 @@
    1.22    // NB: last line lacks \n
    1.23    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    1.24    {
    1.25 +    val char_width = Pretty.char_width_int(text_area.getPainter.getFontMetrics)
    1.26 +
    1.27      val buffer = text_area.getBuffer
    1.28  
    1.29      val p = text_area.offsetToXY(range.start)
    1.30 @@ -186,9 +177,9 @@
    1.31      val end = buffer.getLength
    1.32      val stop = range.stop
    1.33      val (q, r) =
    1.34 -      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
    1.35 +      if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
    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 +        (text_area.offsetToXY(stop - 1), char_width)
    1.39        else (text_area.offsetToXY(stop), 0)
    1.40  
    1.41      if (p != null && q != null && p.x < q.x + r && p.y == q.y)