--- a/src/Pure/PIDE/command.scala Wed Nov 25 13:06:03 2020 +0100
+++ b/src/Pure/PIDE/command.scala Wed Nov 25 13:12:31 2020 +0100
@@ -374,13 +374,6 @@
state
}
- case None
- if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
- val range = command.core_range
- val props = Position.purge(atts)
- val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
- state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
-
case _ => bad(); state
}
case _ => bad(); state