src/Pure/PIDE/command.scala
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)