1.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 28 23:44:43 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 29 13:32:53 2013 +0100
     1.3 @@ -243,14 +243,16 @@
     1.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     1.5      {
     1.6        robust_rendering { rendering =>
     1.7 -        val fm = text_area.getPainter.getFontMetrics
     1.8 +        val painter = text_area.getPainter
     1.9 +        val fm = painter.getFontMetrics
    1.10 +        val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)
    1.11  
    1.12          val (bullet_x, bullet_y, bullet_w, bullet_h) =
    1.13          {
    1.14            val w = fm.charWidth(' ')
    1.15 -          val h = fm.getAscent
    1.16 -          val b = (if (w >= 8) w / 2 else w - 2) max 1
    1.17 -          ((w - b + 1) / 2, (h - b + 1) / 2, w - b, line_height - b)
    1.18 +          val b = (w / 2) max 1
    1.19 +          val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
    1.20 +          ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
    1.21          }
    1.22  
    1.23          for (i <- 0 until physical_lines.length) {