--- a/src/Pure/PIDE/isar_document.scala Tue Sep 07 14:53:05 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Tue Sep 07 15:03:59 2010 +0200
@@ -61,6 +61,12 @@
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
private val exclude_pos = Set(Markup.LOCATION)
+ private def is_state(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case _ => false
+ }
+
def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
{
def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
@@ -73,7 +79,8 @@
case _ => set
}
val set = reported(Set.empty, message)
- if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
+ if (set.isEmpty && !is_state(message))
+ set ++ Position.Range.unapply(message.markup.properties)
else set
}
}