# HG changeset patch
# User wenzelm
# Date 1548951495 -3600
# Node ID 5a8ae7a4b7d038ab8cc3608c6963a8a110ad67bc
# Parent  8608928e54ab0af04fe7ebb6bcefff6b12d62826
added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);

diff -r 8608928e54ab -r 5a8ae7a4b7d0 NEWS
--- a/NEWS	Thu Jan 31 16:56:31 2019 +0100
+++ b/NEWS	Thu Jan 31 17:18:15 2019 +0100
@@ -53,6 +53,9 @@
 entries are structured according to chapter / session names, the open
 operation is redirected to the session ROOT file.
 
+* System option "jedit_text_overview" allows to disable the text
+overview column.
+
 * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
 DejaVu" collection by default, which provides uniform rendering quality
 with the usual Isabelle symbols. Line spacing no longer needs to be
diff -r 8608928e54ab -r 5a8ae7a4b7d0 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Jan 31 16:56:31 2019 +0100
+++ b/src/Tools/jEdit/etc/options	Thu Jan 31 17:18:15 2019 +0100
@@ -36,6 +36,9 @@
 public option jedit_timing_threshold : real = 0.1
   -- "default threshold for timing display (seconds)"
 
+public option jedit_text_overview : bool = true
+  -- "paint text overview column"
+
 
 section "Indentation"
 
diff -r 8608928e54ab -r 5a8ae7a4b7d0 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Jan 31 16:56:31 2019 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Jan 31 17:18:15 2019 +0100
@@ -196,7 +196,8 @@
 
   /* text status overview left of scrollbar */
 
-  private val text_overview = new Text_Overview(this)
+  private val text_overview: Option[Text_Overview] =
+    if (PIDE.options.bool("jedit_text_overview")) Some(new Text_Overview(this)) else None
 
 
   /* main */
@@ -204,7 +205,7 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Raw_Edits =>
-        text_overview.invoke()
+        text_overview.foreach(_.invoke())
 
       case changed: Session.Commands_Changed =>
         val buffer = model.buffer
@@ -216,7 +217,7 @@
               if (changed.assignment ||
                   (changed.nodes.contains(model.node_name) &&
                    changed.commands.exists(snapshot.node.commands.contains)))
-                text_overview.invoke()
+                text_overview.foreach(_.invoke())
 
               JEdit_Lib.invalidate(text_area)
             }
@@ -236,7 +237,9 @@
     text_area.getGutter.addExtension(gutter_painter)
     text_area.addKeyListener(key_listener)
     text_area.addCaretListener(caret_listener)
-    text_area.addLeftOfScrollBar(text_overview); text_area.revalidate(); text_area.repaint()
+    text_overview.foreach(text_area.addLeftOfScrollBar(_))
+    text_area.revalidate()
+    text_area.repaint()
     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
       foreach(text_area.addStructureMatcher(_))
     session.raw_edits += main
@@ -251,8 +254,10 @@
     session.commands_changed -= main
     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
       foreach(text_area.removeStructureMatcher(_))
-    text_overview.revoke(); text_area.removeLeftOfScrollBar(text_overview)
-    text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
+    text_overview.foreach(_.revoke())
+    text_overview.foreach(text_area.removeLeftOfScrollBar(_))
+    text_area.removeCaretListener(caret_listener)
+    delay_caret_update.revoke()
     text_area.removeKeyListener(key_listener)
     text_area.getGutter.removeExtension(gutter_painter)
     rich_text_area.deactivate()