# HG changeset patch
# User wenzelm
# Date 1606306351 -3600
# Node ID eca176f773e021db0a62b5df809fb4244fc6a8b9
# Parent  79a19657c1709c0d1e005dc7d6fdd5e7a7181c26
removed pointless case: messages should always carry proper position;

diff -r 79a19657c170 -r eca176f773e0 src/Pure/PIDE/command.scala
--- 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