# HG changeset patch
# User wenzelm
# Date 1364560373 -3600
# Node ID 564103cb07d545dfdd76ebd1109649093691cad6
# Parent  39896f83c1ab4f66a1db0deb62e90a3c4f5acead
improved centering via strikethrough offset;

diff -r 39896f83c1ab -r 564103cb07d5 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 28 23:44:43 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 29 13:32:53 2013 +0100
@@ -243,14 +243,16 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       robust_rendering { rendering =>
-        val fm = text_area.getPainter.getFontMetrics
+        val painter = text_area.getPainter
+        val fm = painter.getFontMetrics
+        val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)
 
         val (bullet_x, bullet_y, bullet_w, bullet_h) =
         {
           val w = fm.charWidth(' ')
-          val h = fm.getAscent
-          val b = (if (w >= 8) w / 2 else w - 2) max 1
-          ((w - b + 1) / 2, (h - b + 1) / 2, w - b, line_height - b)
+          val b = (w / 2) max 1
+          val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
+          ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
         }
 
         for (i <- 0 until physical_lines.length) {