silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;
--- 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)