src/Tools/jEdit/src/document_view.scala
changeset 44378 81b4af4cfa5a
parent 43661 39fdbd814c7f
child 44379 1079ab6b342b
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Aug 22 12:17:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Aug 22 14:15:52 2011 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* visible line ranges */
     1.8 +  /* visible text range */
     1.9  
    1.10    // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
    1.11    // NB: jEdit already normalizes \r\n and \r to \n
    1.12 @@ -96,14 +96,14 @@
    1.13      Text.Range(start, stop)
    1.14    }
    1.15  
    1.16 -  def screen_lines_range(): Text.Range =
    1.17 +  def visible_range(): Text.Range =
    1.18    {
    1.19      val start = text_area.getScreenLineStartOffset(0)
    1.20      val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
    1.21      proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
    1.22    }
    1.23  
    1.24 -  def invalidate_line_range(range: Text.Range)
    1.25 +  def invalidate_range(range: Text.Range)
    1.26    {
    1.27      text_area.invalidateLineRange(
    1.28        model.buffer.getLineOfOffset(range.start),
    1.29 @@ -224,9 +224,9 @@
    1.30  
    1.31            if (control) init_popup(snapshot, x, y)
    1.32  
    1.33 -          _highlight_range map { case (range, _) => invalidate_line_range(range) }
    1.34 +          _highlight_range map { case (range, _) => invalidate_range(range) }
    1.35            _highlight_range = if (control) subexp_range(snapshot, x, y) else None
    1.36 -          _highlight_range map { case (range, _) => invalidate_line_range(range) }
    1.37 +          _highlight_range map { case (range, _) => invalidate_range(range) }
    1.38          }
    1.39      }
    1.40    }
    1.41 @@ -415,15 +415,15 @@
    1.42            val buffer = model.buffer
    1.43            Isabelle.swing_buffer_lock(buffer) {
    1.44              val (updated, snapshot) = flush_snapshot()
    1.45 -            val visible_range = screen_lines_range()
    1.46 +            val visible = visible_range()
    1.47  
    1.48              if (updated || changed.exists(snapshot.node.commands.contains))
    1.49                overview.repaint()
    1.50  
    1.51 -            if (updated) invalidate_line_range(visible_range)
    1.52 +            if (updated) invalidate_range(visible)
    1.53              else {
    1.54                val visible_cmds =
    1.55 -                snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
    1.56 +                snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
    1.57                if (visible_cmds.exists(changed)) {
    1.58                  for {
    1.59                    line <- 0 until text_area.getVisibleLines