# HG changeset patch
# User wenzelm
# Date 1607256206 -3600
# Node ID ffae996e9c08683a5fda0f598df79cdb1732accd
# Parent  ec0d3a62bb3ba6e591439eba0d5dc7230eead79f
silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;

diff -r ec0d3a62bb3b -r ffae996e9c08 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)