src/Pure/PIDE/command.scala
changeset 49526 6d1465c00f2e
parent 49493 db58490a68ac
child 49527 b96e4a39cc3e
--- a/src/Pure/PIDE/command.scala	Sat Sep 22 17:55:56 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Sep 22 19:16:48 2012 +0200
@@ -48,7 +48,8 @@
                 val props = Position.purge(atts)
                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
-              case XML.Elem(Markup(name, atts), args) =>
+              case XML.Elem(Markup(name, atts), args)
+              if !atts.exists({ case (a, _) => Isabelle_Markup.POSITION_PROPERTIES(a) }) =>
                 val range = command.proper_range
                 val props = Position.purge(atts)
                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))