# HG changeset patch
# User wenzelm
# Date 1348334208 -7200
# Node ID 6d1465c00f2e1f2b3f8c6ca774cbe66add424189
# Parent  e87b42a26991f26753c1ee86e6b53b0e3170970d
more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);

diff -r e87b42a26991 -r 6d1465c00f2e src/Pure/PIDE/command.scala
--- 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))