# HG changeset patch
# User wenzelm
# Date 1283462781 -7200
# Node ID 470fd769ae532c57054bf802ca37186b8ea61b5d
# Parent  6c8d0ea646a635ac9b96342bf80a5f44b42235ec
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;

diff -r 6c8d0ea646a6 -r 470fd769ae53 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Thu Sep 02 23:17:13 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 02 23:26:21 2010 +0200
@@ -58,17 +58,23 @@
 
   /* reported positions */
 
+  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+  private val exclude_pos = Set(Markup.LOCATION)
+
   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] =
       tree match {
         case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
-        if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
-          id == command_id => body.foldLeft(set + range)(reported)
-        case XML.Elem(_, body) => body.foldLeft(set)(reported)
-        case XML.Text(_) => set
+        if include_pos(name) && id == command_id =>
+          body.foldLeft(set + range)(reported)
+        case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
+          body.foldLeft(set)(reported)
+        case _ => set
       }
-    reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
+    val set = reported(Set.empty, message)
+    if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
+    else set
   }
 }