more efficient painting based on cached result;

--- a/src/Pure/PIDE/document.scala	Thu Sep 13 11:13:00 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Sep 13 16:01:42 2012 +0200
@@ -290,6 +290,7 @@
     def convert(range: Text.Range): Text.Range
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
+    def eq_markup(other: Snapshot): Boolean
     def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
       result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
     def select_markup[A](range: Text.Range, elements: Option[Set[String]],
@@ -479,7 +480,8 @@
 
 
     // persistent user-view
-    def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
+    def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
+      : Snapshot =
     {
       val stable = recent_stable
       val latest = history.tip
@@ -503,6 +505,16 @@
         def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
         def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
 
+        def eq_markup(other: Snapshot): Boolean =
+          !is_outdated && !other.is_outdated &&
+            node.commands.size == other.node.commands.size &&
+            ((node.commands.iterator zip other.node.commands.iterator) forall {
+              case (cmd1, cmd2) =>
+                cmd1.source == cmd2.source &&
+                (state.command_state(version, cmd1).markup eq
+                 other.state.command_state(other.version, cmd2).markup)
+            })
+
         def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
           result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
         {

--- a/src/Tools/jEdit/src/text_overview.scala	Thu Sep 13 11:13:00 2012 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Thu Sep 13 16:01:42 2012 +0200
@@ -11,7 +11,7 @@
 
 import scala.annotation.tailrec
 
-import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension}
+import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
 import java.awt.event.{MouseAdapter, MouseEvent}
 import javax.swing.{JPanel, ToolTipManager}
 
@@ -48,6 +48,17 @@
     super.removeNotify
   }
 
+
+  /* painting based on cached result */
+
+  private var cached_colors: List[(Color, Int, Int)] = Nil
+
+  private var last_snapshot = Document.State.init.snapshot()
+  private var last_line_count = 0
+  private var last_char_count = 0
+  private var last_L = 0
+  private var last_H = 0
+
   override def paintComponent(gfx: Graphics)
   {
     super.paintComponent(gfx)
@@ -57,39 +68,64 @@
       Isabelle.buffer_lock(buffer) {
         val snapshot = doc_view.model.snapshot()
 
-        gfx.setColor(getBackground)
-        gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+        if (snapshot.is_outdated) {
+          gfx.setColor(Isabelle_Rendering.color_value("color_outdated"))
+          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+        }
+        else {
+          gfx.setColor(getBackground)
+          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+
+          val line_count = buffer.getLineCount
+          val char_count = buffer.getLength
 
-        val line_count = buffer.getLineCount
-        val char_count = buffer.getLength
+          val L = lines()
+          val H = getHeight()
 
-        val L = lines()
-        val H = getHeight()
+          if (!(line_count == last_line_count && char_count == last_char_count &&
+                L == last_L && H == last_H && (snapshot eq_markup last_snapshot)))
+          {
+            @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
+              : List[(Color, Int, Int)] =
+            {
+              if (l < line_count && h < H) {
+                val p1 = p + H
+                val q1 = q + HEIGHT * L
+                val (l1, h1) =
+                  if (p1 >= q1) (l + 1, h + (p1 - q) / L)
+                  else (l + (q1 - p) / H, h + HEIGHT)
 
-        @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
-        {
-          if (l < line_count && h < H) {
-            val p1 = p + H
-            val q1 = q + HEIGHT * L
-            val (l1, h1) =
-              if (p1 >= q1) (l + 1, h + (p1 - q) / L)
-              else (l + (q1 - p) / H, h + HEIGHT)
+                val start = buffer.getLineStartOffset(l)
+                val end =
+                  if (l1 < line_count) buffer.getLineStartOffset(l1)
+                  else char_count
+                val range = Text.Range(start, end)
 
-            val start = buffer.getLineStartOffset(l)
-            val end =
-              if (l1 < line_count) buffer.getLineStartOffset(l1)
-              else char_count
+                val colors1 =
+                  (Isabelle_Rendering.overview_color(snapshot, range), colors) match {
+                    case (Some(color), (old_color, old_h, old_h1) :: rest)
+                    if color == old_color && old_h1 == h => (color, old_h, h1) :: rest
+                    case (Some(color), _) => (color, h, h1) :: colors
+                    case (None, _) => colors
+                  }
+                loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1)
+              }
+              else colors.reverse
+            }
+            cached_colors = loop(0, 0, 0, 0, Nil)
 
-            Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
-              case None =>
-              case Some(color) =>
-                gfx.setColor(color)
-                gfx.fillRect(0, h, getWidth, h1 - h)
-            }
-            paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
+            last_snapshot = snapshot
+            last_line_count = line_count
+            last_char_count = char_count
+            last_L = L
+            last_H = H
+          }
+
+          for ((color, h, h1) <- cached_colors) {
+            gfx.setColor(color)
+            gfx.fillRect(0, h, getWidth, h1 - h)
           }
         }
-        paint_loop(0, 0, 0, 0)
       }
     }
   }