src/Tools/jEdit/src/document_view.scala
changeset 49408 3cfc114acd05
parent 49407 215ba6884bdf
child 49410 34acbcc33adf
     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)