changeset 73115 | a8e5d7c9a834 |
parent 73031 | f93f0597f4fb |
child 73120 | c3589f2dff31 |
--- a/src/Pure/PIDE/command.scala Sat Jan 09 15:56:09 2021 +0100 +++ b/src/Pure/PIDE/command.scala Sat Jan 09 18:56:53 2021 +0100 @@ -614,7 +614,7 @@ val opt_range = reported_range orElse { if (name == Symbol.Text_Chunk.Default) - Position.Range.unapply(span.absolute_position) + Position.Range.unapply(span.position) else None } opt_range match {