# HG changeset patch
# User wenzelm
# Date 1363880153 -3600
# Node ID 18120e26f8187fd059eaeda806f3162e8fe0bad0
# Parent  0e8012983c4e91601d917c6ccd01a212c6715c8c
eliminated char_width_int to avoid unclear rounding;
clarified integer conversion for margin;

diff -r 0e8012983c4e -r 18120e26f818 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Mar 21 10:05:03 2013 +0100
+++ b/src/Pure/General/pretty.scala	Thu Mar 21 16:35:53 2013 +0100
@@ -84,7 +84,6 @@
   private def metric_default(s: String) = s.length.toDouble
 
   def char_width(metrics: FontMetrics): Double = metrics.stringWidth("mix").toDouble / 3
-  def char_width_int(metrics: FontMetrics): Int = char_width(metrics).round.toInt
 
   def font_metric(metrics: FontMetrics): String => Double =
     if (metrics == null) ((s: String) => s.length.toDouble)
diff -r 0e8012983c4e -r 18120e26f818 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Mar 21 10:05:03 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Mar 21 16:35:53 2013 +0100
@@ -168,7 +168,7 @@
   // NB: last line lacks \n
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   {
-    val char_width = Pretty.char_width_int(text_area.getPainter.getFontMetrics)
+    val char_width = Pretty.char_width(text_area.getPainter.getFontMetrics).round.toInt
 
     val buffer = text_area.getBuffer
 
diff -r 0e8012983c4e -r 18120e26f818 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Mar 21 10:05:03 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Mar 21 16:35:53 2013 +0100
@@ -109,7 +109,7 @@
 
     if (getWidth > 0) {
       val fm = getPainter.getFontMetrics
-      val margin = (getPainter.getWidth / (Pretty.char_width_int(fm) max 1)) max 20
+      val margin = (getPainter.getWidth / (Pretty.char_width(fm).ceil.toInt max 1)) max 20
 
       val base_snapshot = current_base_snapshot
       val base_results = current_base_results
diff -r 0e8012983c4e -r 18120e26f818 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 21 10:05:03 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 21 16:35:53 2013 +0100
@@ -501,7 +501,7 @@
             val offset = caret - text_area.getLineStartOffset(physical_line)
             val x = text_area.offsetToXY(physical_line, offset).x
             gfx.setColor(painter.getCaretColor)
-            gfx.drawRect(x, y, Pretty.char_width_int(fm) - 1, fm.getHeight - 1)
+            gfx.drawRect(x, y, Pretty.char_width(fm).round.toInt - 1, fm.getHeight - 1)
           }
         }
       }