more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);

--- 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))