src/Tools/jEdit/src/document_view.scala
changeset 68728 c07f6fa02c59
parent 66114 c137a9f038a6
child 69775 5a8ae7a4b7d0
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 29 13:18:10 2018 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Jul 31 21:06:09 2018 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4          PIDE.editor.current_command(view, snapshot) match {
     1.5            case Some(command) =>
     1.6              snapshot.node.command_start(command) match {
     1.7 -              case Some(start) => List(snapshot.convert(command.proper_range + start))
     1.8 +              case Some(start) => List(snapshot.convert(command.core_range + start))
     1.9                case None => Nil
    1.10              }
    1.11            case None => Nil