src/Tools/jEdit/src/jedit_lib.scala
changeset 51469 18120e26f818
parent 51078 4e1c940b1fb2
child 51492 eaa1c4cc1106
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Mar 21 10:05:03 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Mar 21 16:35:53 2013 +0100
     1.3 @@ -168,7 +168,7 @@
     1.4    // NB: last line lacks \n
     1.5    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
     1.6    {
     1.7 -    val char_width = Pretty.char_width_int(text_area.getPainter.getFontMetrics)
     1.8 +    val char_width = Pretty.char_width(text_area.getPainter.getFontMetrics).round.toInt
     1.9  
    1.10      val buffer = text_area.getBuffer
    1.11