# HG changeset patch
# User wenzelm
# Date 1407850284 -7200
# Node ID dcb758188aa6e5d2e86e859a2f7c4872634dac06
# Parent  a50837b637dcbbdf9871f8d4c038b0c2dc66bd55
clarified Position.Identified: do not require range from prover, default to command position;

diff -r a50837b637dc -r dcb758188aa6 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Tue Aug 12 14:15:58 2014 +0200
+++ b/src/Pure/General/position.scala	Tue Aug 12 15:31:24 2014 +0200
@@ -81,17 +81,17 @@
       }
   }
 
-  object Reported
+  object Identified
   {
-    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name, Symbol.Range)] =
-      (pos, pos) match {
-        case (Id(id), Range(range)) =>
+    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
+      pos match {
+        case Id(id) =>
           val chunk_name =
             pos match {
               case File(name) => Symbol.Text_Chunk.File(name)
               case _ => Symbol.Text_Chunk.Default
             }
-          Some((id, chunk_name, range))
+          Some((id, chunk_name))
         case _ => None
       }
   }
diff -r a50837b637dc -r dcb758188aa6 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 14:15:58 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 15:31:24 2014 +0200
@@ -163,7 +163,7 @@
       val kind =
         if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
           val name = span.head.source
-          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length))
+          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
           Command_Span.Command_Span(name, pos)
         }
         else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
diff -r a50837b637dc -r dcb758188aa6 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 12 14:15:58 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 12 15:31:24 2014 +0200
@@ -189,8 +189,7 @@
               def bad(): Unit = Output.warning("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(
-                    Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
+                case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) =>
 
                   val target =
                     if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
@@ -198,8 +197,8 @@
                     else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
                     else None
 
-                  target match {
-                    case Some((target_name, target_chunk)) =>
+                  (target, atts) match {
+                    case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
                       target_chunk.incorporate(symbol_range) match {
                         case Some(range) =>
                           val props = Position.purge(atts)
@@ -207,7 +206,7 @@
                           state.add_markup(false, target_name, info)
                         case None => bad(); state
                       }
-                    case None =>
+                    case _ =>
                       // silently ignore excessive reports
                       state
                   }
@@ -232,7 +231,8 @@
               if (Protocol.is_inlined(message)) {
                 for {
                   (chunk_name, chunk) <- command.chunks.iterator
-                  range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
+                  range <- Protocol.message_positions(
+                    self_id, command.position, chunk_name, chunk, message)
                 } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
               }
               st
diff -r a50837b637dc -r dcb758188aa6 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Aug 12 14:15:58 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Aug 12 15:31:24 2014 +0200
@@ -312,17 +312,21 @@
 
   def message_positions(
     self_id: Document_ID.Generic => Boolean,
+    command_position: Position.T,
     chunk_name: Symbol.Text_Chunk.Name,
     chunk: Symbol.Text_Chunk,
     message: XML.Elem): Set[Text.Range] =
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
-        case Position.Reported(id, name, symbol_range)
-        if self_id(id) && name == chunk_name =>
-          chunk.incorporate(symbol_range) match {
-            case Some(range) => set + range
-            case _ => set
+        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
+          Position.Range.unapply(props) orElse Position.Range.unapply(command_position) match {
+            case Some(symbol_range) =>
+              chunk.incorporate(symbol_range) match {
+                case Some(range) => set + range
+                case _ => set
+              }
+            case None => set
           }
         case _ => set
       }