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