# HG changeset patch
# User wenzelm
# Date 1379789912 -7200
# Node ID ef62204a126b011da364d2a7b05138d9bb407d75
# Parent  52578f803d1da07bc310223f45b345165d03fff7
caret range of active text area counts as visible (e.g. relevant for Output after scrolling outside of text view);

diff -r 52578f803d1d -r ef62204a126b src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sat Sep 21 20:56:06 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Sep 21 20:58:32 2013 +0200
@@ -80,9 +80,15 @@
   def perspective(): Text.Perspective =
   {
     Swing_Thread.require()
+
+    val active_caret =
+      if (text_area.getView != null && text_area.getView.getTextArea == text_area)
+        List(JEdit_Lib.point_range(model.buffer, text_area.getCaretPosition))
+      else Nil
+
     val buffer_range = JEdit_Lib.buffer_range(model.buffer)
-    Text.Perspective(
-      for {
+    val visible_lines =
+      (for {
         i <- 0 until text_area.getVisibleLines
         start = text_area.getScreenLineStartOffset(i)
         stop = text_area.getScreenLineEndOffset(i)
@@ -90,7 +96,9 @@
         range <- buffer_range.try_restrict(Text.Range(start, stop))
         if !range.is_singularity
       }
-      yield range)
+      yield range).toList
+
+    Text.Perspective(active_caret ::: visible_lines)
   }
 
   private def update_perspective = new TextAreaExtension