# HG changeset patch
# User wenzelm
# Date 1350916075 -7200
# Node ID 72216713733a38cbb63c40fe4b3806fee480c8bb
# Parent  d9e08e2555f929159c7f4d9a9d5113eddd483d2e
further attempts to cope with large files via option jedit_text_overview_limit;

diff -r d9e08e2555f9 -r 72216713733a src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Oct 22 14:52:38 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Oct 22 16:27:55 2012 +0200
@@ -15,8 +15,8 @@
 option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
-option jedit_text_overview : bool = true
-  -- "paint text overview column (potentially slow for large files)"
+option jedit_text_overview_limit : int = 100000
+  -- "maximum amount of text to visualize in overview column"
 
 
 section "Rendering of Document Content"
diff -r d9e08e2555f9 -r 72216713733a src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Mon Oct 22 14:52:38 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Mon Oct 22 16:27:55 2012 +0200
@@ -41,7 +41,7 @@
 {
   // FIXME avoid hard-wired stuff
   private val relevant_options =
-    Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview",
+    Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
       "jedit_tooltip_font_scale", "jedit_tooltip_margin", "editor_load_delay",
       "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
 
diff -r d9e08e2555f9 -r 72216713733a src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Oct 22 14:52:38 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Oct 22 16:27:55 2012 +0200
@@ -149,6 +149,8 @@
 
   /* command overview */
 
+  val overview_limit = options.int("jedit_text_overview_limit")
+
   def overview_color(range: Text.Range): Option[Color] =
   {
     if (snapshot.is_outdated) None
diff -r d9e08e2555f9 -r 72216713733a src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Mon Oct 22 14:52:38 2012 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Mon Oct 22 16:27:55 2012 +0200
@@ -55,6 +55,7 @@
 
   private var last_snapshot = Document.State.init.snapshot()
   private var last_options = Isabelle.options.value
+  private var last_relevant_range = Text.Range(0)
   private var last_line_count = 0
   private var last_char_count = 0
   private var last_L = 0
@@ -67,10 +68,12 @@
 
     doc_view.rich_text_area.robust_body(()) {
       JEdit_Lib.buffer_lock(buffer) {
-        val snapshot = doc_view.model.snapshot()
+        val rendering = doc_view.get_rendering()
+        val snapshot = rendering.snapshot
+        val options = rendering.options
 
-        if (snapshot.is_outdated || !Isabelle.options.bool("jedit_text_overview")) {
-          gfx.setColor(Isabelle.options.color_value("outdated_color"))
+        if (snapshot.is_outdated) {
+          gfx.setColor(rendering.outdated_color)
           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
         }
         else {
@@ -83,14 +86,20 @@
           val L = lines()
           val H = getHeight()
 
-          val options = Isabelle.options.value
+          val relevant_range =
+            JEdit_Lib.visible_range(text_area) match {
+              case None => Text.Range(0)
+              case Some(visible_range) =>
+                val len = rendering.overview_limit max visible_range.length
+                val start = ((visible_range.start + visible_range.stop - len) / 2) max 0
+                val stop = (start + len) min char_count
+                Text.Range(start, stop)
+            }
 
           if (!(line_count == last_line_count && char_count == last_char_count &&
-                L == last_L && H == last_H && (snapshot eq_markup last_snapshot) &&
-                (options eq last_options)))
+                L == last_L && H == last_H && relevant_range == last_relevant_range &&
+                (snapshot eq_markup last_snapshot) && (options eq last_options)))
           {
-            val rendering = Isabelle_Rendering(snapshot, options)
-
             @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
               : List[(Color, Int, Int)] =
             {
@@ -107,8 +116,11 @@
                   else char_count
                 val range = Text.Range(start, end)
 
+                val range_color =
+                  if (range overlaps relevant_range) rendering.overview_color(range)
+                  else Some(rendering.outdated_color)
                 val colors1 =
-                  (rendering.overview_color(range), colors) match {
+                  (range_color, 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
@@ -122,6 +134,7 @@
 
             last_snapshot = snapshot
             last_options = options
+            last_relevant_range = relevant_range
             last_line_count = line_count
             last_char_count = char_count
             last_L = L