src/Pure/PIDE/document.scala
changeset 68728 c07f6fa02c59
parent 68496 7266fb64de69
child 68836 cf52379c0776
--- a/src/Pure/PIDE/document.scala	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Jul 31 21:06:09 2018 +0200
@@ -1024,7 +1024,7 @@
             blob_name <- cmd.blobs_names.iterator
             if pred(blob_name)
             start <- node.command_start(cmd)
-          } yield convert(cmd.proper_range + start)).toList
+          } yield convert(cmd.core_range + start)).toList
 
         def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
           if (other_node_name.is_theory) {