silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;
authorwenzelm
Sun, 06 Dec 2020 13:03:26 +0100
changeset 72831 ffae996e9c08
parent 72830 ec0d3a62bb3b
child 72832 03803bbfdca3
silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;
src/Pure/PIDE/command.scala
--- 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)