obsolete;
authorwenzelm
Sat, 19 Sep 2015 22:20:08 +0200
changeset 61199 413075a38b9e
parent 61198 459ba5953517
child 61200 a5674da43c2b
obsolete;
src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Sep 19 21:09:38 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Sep 19 22:20:08 2015 +0200
@@ -905,9 +905,6 @@
   text buffer. The graphics is scaled to fit the logical buffer length into
   the given window height. Mouse clicks on the overview area position the
   cursor approximately to the corresponding line of text in the buffer.
-  Repainting the overview in real-time causes problems with big theories, so
-  it is restricted according to the system option @{system_option
-  jedit_text_overview_limit} (in characters).
 
   Another course-grained overview is provided by the \emph{Theories}
   panel, but without direct correspondence to text positions.  A