# HG changeset patch
# User wenzelm
# Date 1346698671 -7200
# Node ID 4e5e48c589eabfbd2c2b66a9dd542336cdfa981d
# Parent  8ab9fb2483a909075c88d829fafcc4838b1ca5fe
more direct access to all-important chunks for text painting;
clarified line_start offset: physical line start not start(i);

diff -r 8ab9fb2483a9 -r 4e5e48c589ea Admin/component_repository/components.sha1
--- a/Admin/component_repository/components.sha1	Mon Sep 03 15:50:41 2012 +0200
+++ b/Admin/component_repository/components.sha1	Mon Sep 03 20:57:51 2012 +0200
@@ -11,6 +11,7 @@
 ed72630f307729df08fdedb095f0af8725f81b9c  jedit_build-20120327.tar.gz
 6425f622625024c1de27f3730d6811f6370a19cd  jedit_build-20120414.tar.gz
 7b012f725ec1cc102dc259df178d511cc7890bba  jedit_build-20120813.tar.gz
+70928b6dc49c38599e7310a532ee924c367d7440  jedit_build-20120903.tar.gz
 6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
 1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb  polyml-5.4.1.tar.gz
 8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
diff -r 8ab9fb2483a9 -r 4e5e48c589ea Admin/components/main
--- a/Admin/components/main	Mon Sep 03 15:50:41 2012 +0200
+++ b/Admin/components/main	Mon Sep 03 20:57:51 2012 +0200
@@ -2,7 +2,7 @@
 cvc3-2.4.1
 e-1.5
 jdk-7u6
-jedit_build-20120813
+jedit_build-20120903
 kodkodi-1.2.16
 polyml-5.4.1
 scala-2.9.2
diff -r 8ab9fb2483a9 -r 4e5e48c589ea src/Tools/jEdit/patches/jedit-4.5.2/chunks
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit-4.5.2/chunks	Mon Sep 03 20:57:51 2012 +0200
@@ -0,0 +1,16 @@
+diff -ru jEdit/org/gjt/sp/jedit/textarea/TextArea.java jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- jEdit/org/gjt/sp/jedit/textarea/TextArea.java       2012-08-13 19:11:04.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java       2012-09-03 19:37:48.000000000 +0200
+@@ -905,6 +905,11 @@
+                return chunkCache.getLineInfo(screenLine).physicalLine;
+        } //}}}
+ 
++       public Chunk getChunksOfScreenLine(int screenLine)
++       {
++               return chunkCache.getLineInfo(screenLine).chunks;
++       }
++
+        //{{{ getScreenLineOfOffset() method
+        /**
+         * Returns the screen (wrapped) line containing the specified offset.
+
diff -r 8ab9fb2483a9 -r 4e5e48c589ea src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 03 15:50:41 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 03 20:57:51 2012 +0200
@@ -161,41 +161,6 @@
 
   /* text */
 
-  private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
-  {
-    val painter = text_area.getPainter
-    val font = painter.getFont
-    val font_context = painter.getFontRenderContext
-
-    // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
-    // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
-    val margin =
-      if (buffer.getStringProperty("wrap") != "soft") 0.0f
-      else {
-        val max = buffer.getIntegerProperty("maxLineLen", 0)
-        if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
-        else painter.getWidth - char_width() * 3
-      }.toFloat
-
-    val out = new ArrayList[Chunk]
-    val handler = new DisplayTokenHandler
-
-    var result = Map[Text.Offset, Chunk]()
-    for (line <- physical_lines) {
-      val line_start = buffer.getLineStartOffset(line)
-
-      out.clear
-      handler.init(painter.getStyles, font_context, painter, out, margin, line_start)
-      buffer.markTokens(line, handler)
-
-      for (i <- 0 until out.size) {
-        val chunk = out.get(i)
-        result += (line_start + chunk.offset -> chunk)
-      }
-    }
-    result
-  }
-
   private def paint_chunk_list(snapshot: Document.Snapshot,
     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
@@ -287,21 +252,20 @@
         val fm = text_area.getPainter.getFontMetrics
         var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
 
-        val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
         for (i <- 0 until physical_lines.length) {
-          if (physical_lines(i) != -1) {
-            val x1 =
-              infos.get(start(i)) match {
-                case None => x0
-                case Some(chunk) =>
-                  gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
-                  val w = paint_chunk_list(snapshot, gfx, start(i), chunk, x0, y0).toInt
-                  x0 + w.toInt
-              }
-            gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
-            orig_text_painter.paintValidLine(gfx,
-              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
-            gfx.setClip(clip)
+          val line = physical_lines(i)
+          if (line != -1) {
+            val screen_line = first_line + i
+            val chunks = text_area.getChunksOfScreenLine(screen_line)
+            if (chunks != null) {
+              val line_start = text_area.getBuffer.getLineStartOffset(line)
+              gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
+              val w = paint_chunk_list(snapshot, gfx, line_start, chunks, x0, y0).toInt
+              gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
+              orig_text_painter.paintValidLine(gfx,
+                screen_line, line, start(i), end(i), y + line_height * i)
+              gfx.setClip(clip)
+            }
           }
           y0 += line_height
         }