tuned signature;
authorwenzelm
Mon Sep 17 18:14:54 2012 +0200 (2012-09-17)
changeset 494097140a738aa49
parent 49408 3cfc114acd05
child 49410 34acbcc33adf
tuned signature;
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 18:06:34 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 18:14:54 2012 +0200
     1.3 @@ -107,5 +107,42 @@
     1.4        buffer.getLineOfOffset(range.start),
     1.5        buffer.getLineOfOffset(range.stop))
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* char width */
    1.10 +
    1.11 +  def char_width(text_area: TextArea): Int =
    1.12 +  {
    1.13 +    val painter = text_area.getPainter
    1.14 +    val font = painter.getFont
    1.15 +    val font_context = painter.getFontRenderContext
    1.16 +    font.getStringBounds(" ", font_context).getWidth.round.toInt
    1.17 +  }
    1.18 +
    1.19 +
    1.20 +  /* graphics range */
    1.21 +
    1.22 +  class Gfx_Range(val x: Int, val y: Int, val length: Int)
    1.23 +
    1.24 +  // NB: jEdit already normalizes \r\n and \r to \n
    1.25 +  // NB: last line lacks \n
    1.26 +  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    1.27 +  {
    1.28 +    val buffer = text_area.getBuffer
    1.29 +
    1.30 +    val p = text_area.offsetToXY(range.start)
    1.31 +
    1.32 +    val end = buffer.getLength
    1.33 +    val stop = range.stop
    1.34 +    val (q, r) =
    1.35 +      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area))
    1.36 +      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    1.37 +        (text_area.offsetToXY(stop - 1), char_width(text_area))
    1.38 +      else (text_area.offsetToXY(stop), 0)
    1.39 +
    1.40 +    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
    1.41 +      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
    1.42 +    else None
    1.43 +  }
    1.44  }
    1.45  
     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 18:06:34 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 18:14:54 2012 +0200
     2.3 @@ -26,38 +26,6 @@
     2.4    private val text_area = doc_view.text_area
     2.5  
     2.6  
     2.7 -  /* graphics range */
     2.8 -
     2.9 -  private def char_width(): 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 -  private class Gfx_Range(val x: Int, val y: Int, val length: Int)
    2.18 -
    2.19 -  // NB: jEdit already normalizes \r\n and \r to \n
    2.20 -  // NB: last line lacks \n
    2.21 -  private def gfx_range(range: Text.Range): Option[Gfx_Range] =
    2.22 -  {
    2.23 -    val p = text_area.offsetToXY(range.start)
    2.24 -
    2.25 -    val end = buffer.getLength
    2.26 -    val stop = range.stop
    2.27 -    val (q, r) =
    2.28 -      if (stop >= end) (text_area.offsetToXY(end), char_width())
    2.29 -      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    2.30 -        (text_area.offsetToXY(stop - 1), char_width())
    2.31 -      else (text_area.offsetToXY(stop), 0)
    2.32 -
    2.33 -    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
    2.34 -      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
    2.35 -    else None
    2.36 -  }
    2.37 -
    2.38 -
    2.39    /* original painters */
    2.40  
    2.41    private def pick_extension(name: String): TextAreaExtension =
    2.42 @@ -124,7 +92,7 @@
    2.43              // background color (1)
    2.44              for {
    2.45                Text.Info(range, color) <- rendering.background1(line_range)
    2.46 -              r <- gfx_range(range)
    2.47 +              r <- JEdit_Lib.gfx_range(text_area, range)
    2.48              } {
    2.49                gfx.setColor(color)
    2.50                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    2.51 @@ -133,7 +101,7 @@
    2.52              // background color (2)
    2.53              for {
    2.54                Text.Info(range, color) <- rendering.background2(line_range)
    2.55 -              r <- gfx_range(range)
    2.56 +              r <- JEdit_Lib.gfx_range(text_area, range)
    2.57              } {
    2.58                gfx.setColor(color)
    2.59                gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
    2.60 @@ -142,7 +110,7 @@
    2.61              // squiggly underline
    2.62              for {
    2.63                Text.Info(range, color) <- rendering.squiggly_underline(line_range)
    2.64 -              r <- gfx_range(range)
    2.65 +              r <- JEdit_Lib.gfx_range(text_area, range)
    2.66              } {
    2.67                gfx.setColor(color)
    2.68                val x0 = (r.x / 2) * 2
    2.69 @@ -291,7 +259,7 @@
    2.70              // foreground color
    2.71              for {
    2.72                Text.Info(range, color) <- rendering.foreground(line_range)
    2.73 -              r <- gfx_range(range)
    2.74 +              r <- JEdit_Lib.gfx_range(text_area, range)
    2.75              } {
    2.76                gfx.setColor(color)
    2.77                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    2.78 @@ -301,7 +269,7 @@
    2.79              for {
    2.80                info <- doc_view.highlight_info()
    2.81                Text.Info(range, color) <- info.try_restrict(line_range)
    2.82 -              r <- gfx_range(range)
    2.83 +              r <- JEdit_Lib.gfx_range(text_area, range)
    2.84              } {
    2.85                gfx.setColor(color)
    2.86                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    2.87 @@ -311,7 +279,7 @@
    2.88              for {
    2.89                info <- doc_view.hyperlink_info()
    2.90                Text.Info(range, _) <- info.try_restrict(line_range)
    2.91 -              r <- gfx_range(range)
    2.92 +              r <- JEdit_Lib.gfx_range(text_area, range)
    2.93              } {
    2.94                gfx.setColor(rendering.hyperlink_color)
    2.95                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
    2.96 @@ -357,7 +325,7 @@
    2.97              val offset = caret - text_area.getLineStartOffset(physical_line)
    2.98              val x = text_area.offsetToXY(physical_line, offset).x
    2.99              gfx.setColor(painter.getCaretColor)
   2.100 -            gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
   2.101 +            gfx.drawRect(x, y, JEdit_Lib.char_width(text_area) - 1, fm.getHeight - 1)
   2.102            }
   2.103          }
   2.104        }