# HG changeset patch
# User wenzelm
# Date 1283263645 -7200
# Node ID c8123e77acc5595865a74430baf77aeef4ae69e7
# Parent  5b4efe90c120a0db07a9aa8f800d86f0dac08fce
tuned commands_changed_actor: more precise/efficient handling of visible screen lines;

diff -r 5b4efe90c120 -r c8123e77acc5 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 31 13:20:12 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 31 16:07:25 2010 +0200
@@ -97,6 +97,27 @@
   }
 
 
+  /* visible line ranges */
+
+  // simplify slightly odd result of TextArea.getLineEndOffset etc.
+  // NB: jEdit already normalizes \r\n and \r to \n
+  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
+  {
+    val stop =
+      if (start < end && end - 1 < model.buffer.getLength &&
+          model.buffer.getSegment(end - 1, 1).charAt(0) == '\n') end - 1
+      else end min model.buffer.getLength
+    Text.Range(start, stop)
+  }
+
+  def screen_lines_range(): Text.Range =
+  {
+    val start = text_area.getScreenLineStartOffset(0)
+    val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
+    proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
+  }
+
+
   /* commands_changed_actor */
 
   private val commands_changed_actor = actor {
@@ -106,23 +127,24 @@
           val buffer = model.buffer
           Isabelle.swing_buffer_lock(buffer) {
             val snapshot = model.snapshot()
-            if (changed.exists(snapshot.node.commands.contains)) {
-              var visible_change = false
-              for ((command, start) <- snapshot.node.command_starts) {
-                if (changed(command)) {
-                  val stop = start + command.length
-                  val line1 = buffer.getLineOfOffset(snapshot.convert(start))
-                  val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
-                  if (line2 >= text_area.getFirstLine &&
-                      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
-                    visible_change = true
-                  text_area.invalidateLineRange(line1, line2)
-                }
-              }
+
+            val visible_range = screen_lines_range()
+            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+            if (visible_cmds.exists(changed)) {
+              for {
+                line <- 0 until text_area.getVisibleLines
+                val start = text_area.getScreenLineStartOffset(line) if start >= 0
+                val end = text_area.getScreenLineEndOffset(line) if end >= 0
+                val range = proper_line_range(start, end)
+                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+                if line_cmds.exists(changed)
+              } text_area.invalidateScreenLineRange(line, line)
               // FIXME danger of deadlock!?
-              if (visible_change) model.buffer.propertiesChanged()
+              // FIXME potentially slow!?
+              model.buffer.propertiesChanged()
 
-              overview.repaint()  // FIXME really paint here!?
+              // FIXME really paint here!?
+              overview.repaint()
             }
           }
 
@@ -134,16 +156,6 @@
 
   /* text_area_extension */
 
-  // simplify slightly odd result of TextArea.getLineEndOffset
-  // NB: jEdit already normalizes \r\n and \r to \n
-  def visible_line_end(start: Text.Offset, end: Text.Offset): Text.Offset =
-  {
-    val end1 = end - 1
-    if (start <= end1 && end1 < model.buffer.getLength &&
-        model.buffer.getSegment(end1, 1).charAt(0) == '\n') end1
-    else end
-  }
-
   private val text_area_extension = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
@@ -157,7 +169,7 @@
           var y = y0
           for (i <- 0 until physical_lines.length) {
             if (physical_lines(i) != -1) {
-              val line_range = Text.Range(start(i), visible_line_end(start(i), end(i)))
+              val line_range = proper_line_range(start(i), end(i))
               val cmds = snapshot.node.command_range(snapshot.revert(line_range))
               for ((command, command_start) <- cmds if !command.is_ignored) {
                 val range = line_range.restrict(snapshot.convert(command.range + command_start))