src/Tools/jEdit/src/isabelle.scala
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)