changeset 54530 | 2c1440f70028 |
parent 54461 | 6c360a6ade0e |
child 55432 | 9c53198dbb1c |
--- a/src/Tools/jEdit/src/document_view.scala Wed Nov 20 15:00:25 2013 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Wed Nov 20 15:53:59 2013 +0100 @@ -82,7 +82,7 @@ PIDE.editor.current_command(view, snapshot) match { case Some(command) => snapshot.node.command_start(command) match { - case Some(start) => List(command.proper_range + start) + case Some(start) => List(snapshot.convert(command.proper_range + start)) case None => Nil } case None => Nil