# HG changeset patch
# User wenzelm
# Date 1349343564 -7200
# Node ID ad2bd4e5a029ba9705db7339478babd228018707
# Parent  3003c87f78144522403e3634be90b87693b58d80
option to bypass potentially slow text overview;

diff -r 3003c87f7814 -r ad2bd4e5a029 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Oct 04 11:07:36 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Oct 04 11:39:24 2012 +0200
@@ -18,6 +18,9 @@
 option jedit_tooltip_dismiss_delay : real = 8.0
   -- "global delay for Swing tooltips"
 
+option jedit_text_overview : bool = true
+  -- "paint text overview column (potentially slow for large files)"
+
 
 section "Rendering of Document Content"
 
diff -r 3003c87f7814 -r ad2bd4e5a029 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Thu Oct 04 11:07:36 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Oct 04 11:39:24 2012 +0200
@@ -41,9 +41,10 @@
 {
   // FIXME avoid hard-wired stuff
   private val relevant_options =
-    Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
-      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay",
-      "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
+    Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview",
+      "jedit_tooltip_font_size", "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay",
+      "editor_load_delay", "editor_input_delay", "editor_output_delay",
+      "editor_update_delay", "editor_reparse_limit")
 
   relevant_options.foreach(Isabelle.options.value.check_name _)
 
diff -r 3003c87f7814 -r ad2bd4e5a029 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Thu Oct 04 11:07:36 2012 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Thu Oct 04 11:39:24 2012 +0200
@@ -69,7 +69,7 @@
       JEdit_Lib.buffer_lock(buffer) {
         val snapshot = doc_view.model.snapshot()
 
-        if (snapshot.is_outdated) {
+        if (snapshot.is_outdated || !Isabelle.options.bool("jedit_text_overview")) {
           gfx.setColor(Isabelle.options.color_value("outdated_color"))
           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
         }