changeset 68728 | c07f6fa02c59 |
parent 67148 | d24dcac5eb4c |
child 71495 | 633a8d52fef2 |
--- a/src/Tools/jEdit/src/isabelle.scala Sun Jul 29 13:18:10 2018 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Jul 31 21:06:09 2018 +0200 @@ -334,7 +334,7 @@ node.command_start(command) match { case Some(start) => JEdit_Lib.buffer_edit(buffer) { - val range = command.proper_range + start + val range = command.core_range + start JEdit_Lib.buffer_edit(buffer) { if (padding) { text_area.moveCaretPosition(start + range.length)