src/Tools/jEdit/src/document_view.scala
changeset 53780 ef62204a126b
parent 53274 1760c01f1c78
child 54325 2c4155003352
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Sep 21 20:56:06 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Sep 21 20:58:32 2013 +0200
     1.3 @@ -80,9 +80,15 @@
     1.4    def perspective(): Text.Perspective =
     1.5    {
     1.6      Swing_Thread.require()
     1.7 +
     1.8 +    val active_caret =
     1.9 +      if (text_area.getView != null && text_area.getView.getTextArea == text_area)
    1.10 +        List(JEdit_Lib.point_range(model.buffer, text_area.getCaretPosition))
    1.11 +      else Nil
    1.12 +
    1.13      val buffer_range = JEdit_Lib.buffer_range(model.buffer)
    1.14 -    Text.Perspective(
    1.15 -      for {
    1.16 +    val visible_lines =
    1.17 +      (for {
    1.18          i <- 0 until text_area.getVisibleLines
    1.19          start = text_area.getScreenLineStartOffset(i)
    1.20          stop = text_area.getScreenLineEndOffset(i)
    1.21 @@ -90,7 +96,9 @@
    1.22          range <- buffer_range.try_restrict(Text.Range(start, stop))
    1.23          if !range.is_singularity
    1.24        }
    1.25 -      yield range)
    1.26 +      yield range).toList
    1.27 +
    1.28 +    Text.Perspective(active_caret ::: visible_lines)
    1.29    }
    1.30  
    1.31    private def update_perspective = new TextAreaExtension