more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations;
misc tuning;

--- a/src/Pure/PIDE/document.scala	Fri Jul 02 21:48:54 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Jul 03 20:20:13 2010 +0200
@@ -14,13 +14,13 @@
 {
   /* command start positions */
 
-  def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
+  def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
   {
-    var offset = 0
-    for (cmd <- commands.iterator) yield {
-      val start = offset
-      offset += cmd.length
-      (cmd, start)
+    var i = offset
+    for (command <- commands) yield {
+      val start = i
+      i += command.length
+      (command, start)
     }
   }
 
@@ -60,9 +60,10 @@
     {
       eds match {
         case e :: es =>
-          command_starts(commands).find {   // FIXME relative search!
+          command_starts(commands.iterator).find {
             case (cmd, cmd_start) =>
-              e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
+              e.can_edit(cmd.source, cmd_start) ||
+                e.is_insert && e.start == cmd_start + cmd.length
           } match {
             case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
               val (rest, text) = e.edit(cmd.source, cmd_start)
@@ -144,7 +145,7 @@
 {
   /* command ranges */
 
-  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
+  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands.iterator)
 
   def command_start(cmd: Command): Option[Int] =
     command_starts.find(_._1 == cmd).map(_._2)

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jul 02 21:48:54 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Jul 03 20:20:13 2010 +0200
@@ -95,14 +95,6 @@
   def to_current(doc: Document, offset: Int): Int =
     (offset /: changes_from(doc)) ((i, change) => change after i)
 
-  def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
-  {
-    val start = doc.command_start(cmd).get  // FIXME total?
-    val stop = start + cmd.length
-    (buffer.getLineOfOffset(to_current(doc, start)),
-     buffer.getLineOfOffset(to_current(doc, stop)))
-  }
-
 
   /* text edits */
 

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Jul 02 21:48:54 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Jul 03 20:20:13 2010 +0200
@@ -104,13 +104,10 @@
       react {
         case Command_Set(changed) =>
           Swing_Thread.now {
+            // FIXME cover doc states as well!!?
             val document = model.recent_document()
-            // FIXME cover doc states as well!!?
-            for (command <- changed if document.commands.contains(command)) {
-              update_syntax(document, command)
-              invalidate_line(document, command)
-              overview.repaint()
-            }
+            if (changed.exists(document.commands.contains))
+              full_repaint(document, changed)
           }
 
         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
@@ -118,34 +115,82 @@
     }
   }
 
+  def full_repaint(document: Document, changed: Set[Command])
+  {
+    Swing_Thread.assert()
+
+    val buffer = model.buffer
+    var visible_change = false
+
+    for ((command, start) <- document.command_starts) {
+      if (changed(command)) {
+        val stop = start + command.length
+        val line1 = buffer.getLineOfOffset(model.to_current(document, start))
+        val line2 = buffer.getLineOfOffset(model.to_current(document, stop))
+        if (line2 >= text_area.getFirstLine &&
+            line1 <= text_area.getFirstLine + text_area.getVisibleLines)
+          visible_change = true
+        text_area.invalidateLineRange(line1, line2)
+      }
+    }
+    if (visible_change) model.buffer.propertiesChanged()
+
+    overview.repaint()  // FIXME paint here!?
+  }
+
 
   /* text_area_extension */
 
   private val text_area_extension = new TextAreaExtension
   {
-    override def paintValidLine(gfx: Graphics2D,
-      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+    override def paintScreenLineRange(gfx: Graphics2D,
+      first_line: Int, last_line: Int, physical_lines: Array[Int],
+      start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
     {
-      val document = model.recent_document()
-      def from_current(pos: Int) = model.from_current(document, pos)
-      def to_current(pos: Int) = model.to_current(document, pos)
+      Swing_Thread.now {
+        val document = model.recent_document()
+        def from_current(pos: Int) = model.from_current(document, pos)
+        def to_current(pos: Int) = model.to_current(document, pos)
 
-      val line_end = model.visible_line_end(start, end)
-      val line_height = text_area.getPainter.getFontMetrics.getHeight
+        val command_range: Iterable[(Command, Int)] =
+        {
+          val range = document.command_range(from_current(start(0)))
+          if (range.hasNext) {
+            val (cmd0, start0) = range.next
+            new Iterable[(Command, Int)] {
+              def iterator = Document.command_starts(document.commands.iterator(cmd0), start0)
+            }
+          }
+          else Iterable.empty
+        }
 
-      val saved_color = gfx.getColor
-      try {
-        for ((command, command_start) <-
-          document.command_range(from_current(start), from_current(line_end)) if !command.is_ignored)
-        {
-          val p = text_area.offsetToXY(start max to_current(command_start))
-          val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
-          assert(p.y == q.y)
-          gfx.setColor(Document_View.choose_color(document, command))
-          gfx.fillRect(p.x, y, q.x - p.x, line_height)
+        val saved_color = gfx.getColor
+        try {
+          var y = y0
+          for (i <- 0 until physical_lines.length) {
+            if (physical_lines(i) != -1) {
+              val line_start = start(i)
+              val line_end = model.visible_line_end(line_start, end(i))
+
+              val a = from_current(line_start)
+              val b = from_current(line_end)
+              val cmds = command_range.iterator.
+                dropWhile { case (cmd, c) => c + cmd.length <= a } .
+                takeWhile { case (_, c) => c < b }
+
+              for ((command, command_start) <- cmds if !command.is_ignored) {
+                val p = text_area.offsetToXY(line_start max to_current(command_start))
+                val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
+                assert(p.y == q.y)
+                gfx.setColor(Document_View.choose_color(document, command))
+                gfx.fillRect(p.x, y, q.x - p.x, line_height)
+              }
+            }
+            y += line_height
+          }
         }
+        finally { gfx.setColor(saved_color) }
       }
-      finally { gfx.setColor(saved_color) }
     }
 
     override def getToolTipText(x: Int, y: Int): String =
@@ -186,30 +231,6 @@
   }
 
 
-  /* (re)painting */
-
-  private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
-  // FIXME update_delay property
-
-  private def update_syntax(document: Document, cmd: Command)
-  {
-    val (line1, line2) = model.lines_of_command(document, cmd)
-    if (line2 >= text_area.getFirstLine &&
-      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
-        update_delay()
-  }
-
-  private def invalidate_line(document: Document, cmd: Command) =
-  {
-    val (start, stop) = model.lines_of_command(document, cmd)
-    text_area.invalidateLineRange(start, stop)
-  }
-
-  private def invalidate_all() =
-    text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
-      text_area.getLastPhysicalLine)
-
-
   /* overview of command status left of scrollbar */
 
   private val overview = new JPanel(new BorderLayout)
@@ -252,9 +273,9 @@
       val buffer = model.buffer
       val document = model.recent_document()
       def to_current(pos: Int) = model.to_current(document, pos)
-      val saved_color = gfx.getColor
+      val saved_color = gfx.getColor  // FIXME needed!?
       try {
-        for ((command, start) <- document.command_range(0) if !command.is_ignored) {
+        for ((command, start) <- document.command_starts if !command.is_ignored) {
           val line1 = buffer.getLineOfOffset(to_current(start))
           val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
           val y = line_to_y(line1)