# HG changeset patch
# User wenzelm
# Date 1283864639 -7200
# Node ID 04ad0fed81f512cc6d7d7cb90490333866918a06
# Parent  18cdf28333712870826d2ac4020f5ef95e451859
Isar_Document.reported_positions: exclude proof state output;

diff -r 18cdf2833371 -r 04ad0fed81f5 src/Pure/PIDE/isar_document.scala
--- 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
   }
 }