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) {