changeset 72831 | ffae996e9c08 |
parent 72827 | 1975f397eabb |
child 72846 | a23e0964f3c3 |
--- a/src/Pure/PIDE/command.scala Sat Dec 05 19:24:36 2020 +0000 +++ b/src/Pure/PIDE/command.scala Sun Dec 06 13:03:26 2020 +0100 @@ -322,7 +322,8 @@ else None (target, target_range) match { - case (Some((target_name, target_chunk)), Some(symbol_range)) => + case (Some((target_name, target_chunk)), Some(symbol_range)) + if !symbol_range.is_singularity => target_chunk.incorporate(symbol_range) match { case Some(range) => val props = atts.filterNot(Markup.position_property)