# HG changeset patch
# User wenzelm
# Date 1283253612 -7200
# Node ID 5b4efe90c120a0db07a9aa8f800d86f0dac08fce
# Parent  dde403450419e493db4e938d41443fbc8fca59fb
simplified/clarified Document_View.text_area_extension;
tuned Document.Node.block_size, trading some space for better time;

diff -r dde403450419 -r 5b4efe90c120 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 31 12:49:40 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 31 13:20:12 2010 +0200
@@ -56,7 +56,7 @@
     }
   }
 
-  private val block_size = 4096
+  private val block_size = 1024
 
   class Node(val commands: Linear_Set[Command])
   {
diff -r dde403450419 -r 5b4efe90c120 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Aug 31 12:49:40 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Aug 31 13:20:12 2010 +0200
@@ -190,19 +190,6 @@
 
 class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
 {
-  /* visible line end */
-
-  // 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 < buffer.getLength &&
-        buffer.getSegment(end1, 1).charAt(0) == '\n') end1
-    else end
-  }
-
-
   /* pending text edits */
 
   object pending_edits  // owned by Swing thread
diff -r dde403450419 -r 5b4efe90c120 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 31 12:49:40 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 31 13:20:12 2010 +0200
@@ -134,6 +134,16 @@
 
   /* 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,
@@ -142,40 +152,17 @@
     {
       Isabelle.swing_buffer_lock(model.buffer) {
         val snapshot = model.snapshot()
-
-        val command_range: Iterable[(Command, Text.Offset)] =
-        {
-          val range = snapshot.node.command_range(snapshot.revert(start(0)))
-          if (range.hasNext) {
-            val (cmd0, start0) = range.next
-            new Iterable[(Command, Text.Offset)] {
-              def iterator =
-                Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
-            }
-          }
-          else Iterable.empty
-        }
-
         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 = snapshot.revert(line_start)
-              val b = snapshot.revert(line_end)
-              val cmds = command_range.iterator.
-                dropWhile { case (cmd, c) => c + cmd.length <= a } .
-                takeWhile { case (_, c) => c < b }
-
+              val line_range = Text.Range(start(i), visible_line_end(start(i), end(i)))
+              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
               for ((command, command_start) <- cmds if !command.is_ignored) {
-                val p =
-                  text_area.offsetToXY(line_start max snapshot.convert(command_start))
-                val q =
-                  text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
-                if (p.y != q.y) System.err.println("Unexpected coordinates: " + p + ", " + q)
+                val range = line_range.restrict(snapshot.convert(command.range + command_start))
+                val p = text_area.offsetToXY(range.start)
+                val q = text_area.offsetToXY(range.stop)
                 gfx.setColor(Document_View.choose_color(snapshot, command))
                 gfx.fillRect(p.x, y, q.x - p.x, line_height)
               }