1.1 --- a/src/Pure/General/pretty.scala	Sat Jan 12 18:13:28 2013 +0100
     1.2 +++ b/src/Pure/General/pretty.scala	Sat Jan 12 19:53:24 2013 +0100
     1.3 @@ -14,7 +14,6 @@
     1.4  {
     1.5    /* spaces */
     1.6  
     1.7 -  val spc = ' '
     1.8    val space = " "
     1.9  
    1.10    private val static_spaces = space * 4000
    1.11 @@ -84,10 +83,13 @@
    1.12    private val margin_default = 76
    1.13    private def metric_default(s: String) = s.length.toDouble
    1.14  
    1.15 +  def char_width(metrics: FontMetrics): Double = metrics.stringWidth("mix").toDouble / 3
    1.16 +  def char_width_int(metrics: FontMetrics): Int = char_width(metrics).round.toInt
    1.17 +
    1.18    def font_metric(metrics: FontMetrics): String => Double =
    1.19      if (metrics == null) ((s: String) => s.length.toDouble)
    1.20      else {
    1.21 -      val unit = metrics.charWidth(spc).toDouble
    1.22 +      val unit = char_width(metrics)
    1.23        ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
    1.24      }
    1.25  

     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Jan 12 18:13:28 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Jan 12 19:53:24 2013 +0100
     2.3 @@ -160,17 +160,6 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* char width */
     2.8 -
     2.9 -  def char_width(text_area: TextArea): Int =
    2.10 -  {
    2.11 -    val painter = text_area.getPainter
    2.12 -    val font = painter.getFont
    2.13 -    val font_context = painter.getFontRenderContext
    2.14 -    font.getStringBounds(" ", font_context).getWidth.round.toInt
    2.15 -  }
    2.16 -
    2.17 -
    2.18    /* graphics range */
    2.19  
    2.20    case class Gfx_Range(val x: Int, val y: Int, val length: Int)
    2.21 @@ -179,6 +168,8 @@
    2.22    // NB: last line lacks \n
    2.23    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    2.24    {
    2.25 +    val char_width = Pretty.char_width_int(text_area.getPainter.getFontMetrics)
    2.26 +
    2.27      val buffer = text_area.getBuffer
    2.28  
    2.29      val p = text_area.offsetToXY(range.start)
    2.30 @@ -186,9 +177,9 @@
    2.31      val end = buffer.getLength
    2.32      val stop = range.stop
    2.33      val (q, r) =
    2.34 -      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
    2.35 +      if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
    2.36        else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    2.37 -        (text_area.offsetToXY(stop - 1), char_width(text_area))
    2.38 +        (text_area.offsetToXY(stop - 1), char_width)
    2.39        else (text_area.offsetToXY(stop), 0)
    2.40  
    2.41      if (p != null && q != null && p.x < q.x + r && p.y == q.y)

     3.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jan 12 18:13:28 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jan 12 19:53:24 2013 +0100
     3.3 @@ -107,13 +107,12 @@
     3.4  
     3.5        getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
     3.6  
     3.7 -      val font_metrics = getPainter.getFontMetrics(font)
     3.8 -      val margin =
     3.9 -        ((getWidth - getGutter.getWidth) / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
    3.10 +      val fm = getPainter.getFontMetrics
    3.11 +      val margin = ((getWidth - getGutter.getWidth) / (Pretty.char_width_int(fm) max 1) - 2) max 20
    3.12  
    3.13        val base_snapshot = current_base_snapshot
    3.14        val base_results = current_base_results
    3.15 -      val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
    3.16 +      val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(fm))
    3.17  
    3.18        future_rendering.map(_.cancel(true))
    3.19        future_rendering = Some(default_thread_pool.submit(() =>

     4.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jan 12 18:13:28 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jan 12 19:53:24 2013 +0100
     4.3 @@ -96,17 +96,15 @@
     4.4    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
     4.5  
     4.6    {
     4.7 -    val font_metrics = pretty_text_area.getPainter.getFontMetrics
     4.8 +    val fm = pretty_text_area.getPainter.getFontMetrics
     4.9      val margin = rendering.tooltip_margin
    4.10      val lines =
    4.11 -      XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
    4.12 +      XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
    4.13          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
    4.14  
    4.15      val bounds = rendering.tooltip_bounds
    4.16 -    val w =
    4.17 -      (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen_bounds.width * bounds).toInt
    4.18 -    val h =
    4.19 -      (font_metrics.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
    4.20 +    val w = (Pretty.char_width_int(fm) * (margin + 2)) min (screen_bounds.width * bounds).toInt
    4.21 +    val h = (fm.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
    4.22      pretty_text_area.setPreferredSize(new Dimension(w, h))
    4.23      window.pack
    4.24  

     5.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Jan 12 18:13:28 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jan 12 19:53:24 2013 +0100
     5.3 @@ -490,7 +490,7 @@
     5.4              val offset = caret - text_area.getLineStartOffset(physical_line)
     5.5              val x = text_area.offsetToXY(physical_line, offset).x
     5.6              gfx.setColor(painter.getCaretColor)
     5.7 -            gfx.drawRect(x, y, JEdit_Lib.char_width(text_area) - 1, fm.getHeight - 1)
     5.8 +            gfx.drawRect(x, y, Pretty.char_width_int(fm) - 1, fm.getHeight - 1)
     5.9            }
    5.10          }
    5.11        }