src/Tools/jEdit/src/document_view.scala
changeset 54325 2c4155003352
parent 53780 ef62204a126b
child 54441 3d37b2957a3e
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Oct 11 12:06:26 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Oct 11 20:45:21 2013 +0200
     1.3 @@ -77,14 +77,25 @@
     1.4  
     1.5    /* perspective */
     1.6  
     1.7 -  def perspective(): Text.Perspective =
     1.8 +  def perspective(snapshot: Document.Snapshot): Text.Perspective =
     1.9    {
    1.10      Swing_Thread.require()
    1.11  
    1.12 -    val active_caret =
    1.13 -      if (text_area.getView != null && text_area.getView.getTextArea == text_area)
    1.14 -        List(JEdit_Lib.point_range(model.buffer, text_area.getCaretPosition))
    1.15 +    val active_command =
    1.16 +    {
    1.17 +      val view = text_area.getView
    1.18 +      if (view != null && view.getTextArea == text_area) {
    1.19 +        PIDE.editor.current_command(view, snapshot) match {
    1.20 +          case Some(command) =>
    1.21 +            snapshot.node.command_start(command) match {
    1.22 +              case Some(start) => List(command.proper_range + start)
    1.23 +              case None => Nil
    1.24 +            }
    1.25 +          case None => Nil
    1.26 +        }
    1.27 +      }
    1.28        else Nil
    1.29 +    }
    1.30  
    1.31      val buffer_range = JEdit_Lib.buffer_range(model.buffer)
    1.32      val visible_lines =
    1.33 @@ -98,7 +109,7 @@
    1.34        }
    1.35        yield range).toList
    1.36  
    1.37 -    Text.Perspective(active_caret ::: visible_lines)
    1.38 +    Text.Perspective(active_command ::: visible_lines)
    1.39    }
    1.40  
    1.41    private def update_perspective = new TextAreaExtension