Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;

--- a/src/Pure/PIDE/command.scala	Tue Sep 07 16:08:29 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 07 16:40:30 2010 +0200
@@ -60,8 +60,8 @@
           atts match {
             case Markup.Serial(i) =>
               val result = XML.Elem(Markup(name, Position.purge(atts)), body)
-              (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
-                (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
+              (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
+                (st, range) => st.add_markup(Text.Info(range, result)))
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }

--- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 16:08:29 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 16:40:30 2010 +0200
@@ -67,20 +67,21 @@
       case _ => false
     }
 
-  def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
+  def reported_positions(command: Command, 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 include_pos(name) && id == command_id =>
-          body.foldLeft(set + range)(reported)
+        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
+        if include_pos(name) && id == command.id =>
+          val range = command.decode(raw_range).restrict(command.range)
+          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
         case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
           body.foldLeft(set)(reported)
         case _ => set
       }
     val set = reported(Set.empty, message)
     if (set.isEmpty && !is_state(message))
-      set ++ Position.Range.unapply(message.markup.properties)
+      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
     else set
   }
 }