1.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 14:53:05 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 15:03:59 2010 +0200
     1.3 @@ -61,6 +61,12 @@
     1.4    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     1.5    private val exclude_pos = Set(Markup.LOCATION)
     1.6  
     1.7 +  private def is_state(msg: XML.Tree): Boolean =
     1.8 +    msg match {
     1.9 +      case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    1.10 +      case _ => false
    1.11 +    }
    1.12 +
    1.13    def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
    1.14    {
    1.15      def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.16 @@ -73,7 +79,8 @@
    1.17          case _ => set
    1.18        }
    1.19      val set = reported(Set.empty, message)
    1.20 -    if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
    1.21 +    if (set.isEmpty && !is_state(message))
    1.22 +      set ++ Position.Range.unapply(message.markup.properties)
    1.23      else set
    1.24    }
    1.25  }