tuned signature;
authorwenzelm
Mon Sep 17 18:06:34 2012 +0200 (2012-09-17)
changeset 494083cfc114acd05
parent 49407 215ba6884bdf
child 49409 7140a738aa49
tuned signature;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 17:56:10 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 18:06:34 2012 +0200
     1.3 @@ -88,31 +88,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* visible text range */
     1.8 -
     1.9 -  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
    1.10 -  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
    1.11 -    Text.Range(start, end min model.buffer.getLength)
    1.12 -
    1.13 -  def visible_range(): Option[Text.Range] =
    1.14 -  {
    1.15 -    val n = text_area.getVisibleLines
    1.16 -    if (n > 0) {
    1.17 -      val start = text_area.getScreenLineStartOffset(0)
    1.18 -      val raw_end = text_area.getScreenLineEndOffset(n - 1)
    1.19 -      Some(proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength))
    1.20 -    }
    1.21 -    else None
    1.22 -  }
    1.23 -
    1.24 -  def invalidate_range(range: Text.Range)
    1.25 -  {
    1.26 -    text_area.invalidateLineRange(
    1.27 -      model.buffer.getLineOfOffset(range.start),
    1.28 -      model.buffer.getLineOfOffset(range.stop))
    1.29 -  }
    1.30 -
    1.31 -
    1.32    /* perspective */
    1.33  
    1.34    def perspective(): Text.Perspective =
    1.35 @@ -156,7 +131,7 @@
    1.36        val old_info = the_info
    1.37        if (new_info != old_info) {
    1.38          for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
    1.39 -          invalidate_range(range)
    1.40 +          JEdit_Lib.invalidate_range(text_area, range)
    1.41          the_info = new_info
    1.42        }
    1.43      }
    1.44 @@ -249,12 +224,13 @@
    1.45          val FOLD_MARKER_SIZE = 12
    1.46  
    1.47          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    1.48 -          JEdit_Lib.buffer_lock(model.buffer) {
    1.49 +          val buffer = model.buffer
    1.50 +          JEdit_Lib.buffer_lock(buffer) {
    1.51              val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
    1.52  
    1.53              for (i <- 0 until physical_lines.length) {
    1.54                if (physical_lines(i) != -1) {
    1.55 -                val line_range = proper_line_range(start(i), end(i))
    1.56 +                val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
    1.57  
    1.58                  // gutter icons
    1.59                  rendering.gutter_message(line_range) match {
    1.60 @@ -318,9 +294,9 @@
    1.61                       changed.commands.exists(snapshot.node.commands.contains)))
    1.62                    Swing_Thread.later { overview.delay_repaint.invoke() }
    1.63  
    1.64 -                visible_range() match {
    1.65 +                JEdit_Lib.visible_range(text_area) match {
    1.66                    case Some(visible) =>
    1.67 -                    if (changed.assignment) invalidate_range(visible)
    1.68 +                    if (changed.assignment) JEdit_Lib.invalidate_range(text_area, visible)
    1.69                      else {
    1.70                        val visible_cmds =
    1.71                          snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
    1.72 @@ -329,7 +305,7 @@
    1.73                            line <- 0 until text_area.getVisibleLines
    1.74                            start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.75                            end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.76 -                          range = proper_line_range(start, end)
    1.77 +                          range = JEdit_Lib.proper_line_range(buffer, start, end)
    1.78                            line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    1.79                            if line_cmds.exists(changed.commands)
    1.80                          } text_area.invalidateScreenLineRange(line, line)
     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 17:56:10 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 18:06:34 2012 +0200
     2.3 @@ -77,5 +77,35 @@
     2.4        }
     2.5        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
     2.6      }
     2.7 +
     2.8 +
     2.9 +  /* proper line range */
    2.10 +
    2.11 +  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
    2.12 +  def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range =
    2.13 +    Text.Range(start, end min buffer.getLength)
    2.14 +
    2.15 +
    2.16 +  /* visible text range */
    2.17 +
    2.18 +  def visible_range(text_area: TextArea): Option[Text.Range] =
    2.19 +  {
    2.20 +    val buffer = text_area.getBuffer
    2.21 +    val n = text_area.getVisibleLines
    2.22 +    if (n > 0) {
    2.23 +      val start = text_area.getScreenLineStartOffset(0)
    2.24 +      val raw_end = text_area.getScreenLineEndOffset(n - 1)
    2.25 +      Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength))
    2.26 +    }
    2.27 +    else None
    2.28 +  }
    2.29 +
    2.30 +  def invalidate_range(text_area: TextArea, range: Text.Range)
    2.31 +  {
    2.32 +    val buffer = text_area.getBuffer
    2.33 +    text_area.invalidateLineRange(
    2.34 +      buffer.getLineOfOffset(range.start),
    2.35 +      buffer.getLineOfOffset(range.stop))
    2.36 +  }
    2.37  }
    2.38  
     3.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 17:56:10 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 18:06:34 2012 +0200
     3.3 @@ -119,7 +119,7 @@
     3.4  
     3.5          for (i <- 0 until physical_lines.length) {
     3.6            if (physical_lines(i) != -1) {
     3.7 -            val line_range = doc_view.proper_line_range(start(i), end(i))
     3.8 +            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
     3.9  
    3.10              // background color (1)
    3.11              for {
    3.12 @@ -286,7 +286,7 @@
    3.13        robust_rendering { rendering =>
    3.14          for (i <- 0 until physical_lines.length) {
    3.15            if (physical_lines(i) != -1) {
    3.16 -            val line_range = doc_view.proper_line_range(start(i), end(i))
    3.17 +            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
    3.18  
    3.19              // foreground color
    3.20              for {