author | wenzelm |
Sat, 05 Dec 2020 19:09:39 +0100 | |
changeset 72827 | 1975f397eabb |
parent 72826 | fa5d8f486380 |
child 72828 | 18bc50e58e38 |
--- a/src/Pure/PIDE/command.scala Sat Dec 05 18:14:55 2020 +0100 +++ b/src/Pure/PIDE/command.scala Sat Dec 05 19:09:39 2020 +0100 @@ -594,7 +594,7 @@ val opt_range = reported_range orElse { if (name == Symbol.Text_Chunk.Default) - Position.Range.unapply(span.position) + Position.Range.unapply(span.absolute_position) else None } opt_range match {