src/Tools/jEdit/src/jedit_lib.scala
changeset 51492 eaa1c4cc1106
parent 51469 18120e26f818
child 51507 ebd5366e7a42
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Mar 23 13:04:28 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Mar 23 13:12:39 2013 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  import org.gjt.sp.jedit.{jEdit, Buffer, View}
     1.6  import org.gjt.sp.jedit.buffer.JEditBuffer
     1.7 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     1.8 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
     1.9  
    1.10  
    1.11  object JEdit_Lib
    1.12 @@ -168,7 +168,8 @@
    1.13    // NB: last line lacks \n
    1.14    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    1.15    {
    1.16 -    val char_width = Pretty.char_width(text_area.getPainter.getFontMetrics).round.toInt
    1.17 +    val metric = JEdit_Lib.pretty_metric(text_area.getPainter)
    1.18 +    val char_width = (metric.unit * metric.average).round.toInt
    1.19  
    1.20      val buffer = text_area.getBuffer
    1.21  
    1.22 @@ -203,5 +204,18 @@
    1.23        case _ => None
    1.24      }
    1.25    }
    1.26 +
    1.27 +
    1.28 +  /* pretty text metric */
    1.29 +
    1.30 +  def string_width(painter: TextAreaPainter, s: String): Double =
    1.31 +    painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
    1.32 +
    1.33 +  def pretty_metric(painter: TextAreaPainter): Pretty.Metric =
    1.34 +    new Pretty.Metric {
    1.35 +      val unit = string_width(painter, Pretty.space)
    1.36 +      val average = string_width(painter, "mix") / (3 * unit)
    1.37 +      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(painter, s) / unit
    1.38 +    }
    1.39  }
    1.40