# HG changeset patch
# User wenzelm
# Date 1392127513 -3600
# Node ID 4a50f9e70dc12e93b550319bce545e1fcc494233
# Parent  eae296b5ef3305ebc1bcc0592584a060eb644715
report (but ignore) markup within auxiliary files;

diff -r eae296b5ef33 -r 4a50f9e70dc1 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Tue Feb 11 12:08:44 2014 +0100
+++ b/src/Pure/General/position.scala	Tue Feb 11 15:05:13 2014 +0100
@@ -75,11 +75,12 @@
       }
   }
 
-  object Id_Range
+  object Reported
   {
-    def unapply(pos: T): Option[(Long, Text.Range)] =
+    def unapply(pos: T): Option[(Long, String, Text.Range)] =
       (pos, pos) match {
-        case (Id(id), Range(range)) => Some((id, range))
+        case (Id(id), Range(range)) =>
+          Some((id, File.unapply(pos).getOrElse(""), range))
         case _ => None
       }
   }
diff -r eae296b5ef33 -r 4a50f9e70dc1 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Feb 11 12:08:44 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Tue Feb 11 15:05:13 2014 +0100
@@ -102,8 +102,14 @@
           fun make_file src_path (Exn.Res (_, NONE)) =
                 Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
             | make_file src_path (Exn.Res (file, SOME text)) =
-                let val _ = Position.report pos (Markup.path file)
-                in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
+                let
+                  val _ = Position.report pos (Markup.path file);
+                  val file_pos =
+                    Position.file file (*sic!*) |>
+                    (case Position.get_id (Position.thread_data ()) of
+                      NONE => I
+                    | SOME exec_id => Position.put_id exec_id);
+                in Exn.Res {src_path = src_path, text = text, pos = file_pos} end
             | make_file _ (Exn.Exn e) = Exn.Exn e;
 
           val src_paths = Keyword.command_files cmd path;
diff -r eae296b5ef33 -r 4a50f9e70dc1 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Feb 11 12:08:44 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Feb 11 15:05:13 2014 +0100
@@ -94,8 +94,8 @@
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
-              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
-              if (id == command.id || id == alt_id) &&
+              case XML.Elem(Markup(name, atts @ Position.Reported(id, file, raw_range)), args)
+              if (id == command.id || id == alt_id) && file == "" &&
                   command.range.contains(command.decode(raw_range)) =>
                 val range = command.decode(raw_range)
                 val props = Position.purge(atts)
diff -r eae296b5ef33 -r 4a50f9e70dc1 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Feb 11 12:08:44 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Feb 11 15:05:13 2014 +0100
@@ -285,11 +285,11 @@
 
     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
-        case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body)
-        if include_pos(name) && id == command.id => elem_positions(range, set, body)
+        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file, range)), _, body)
+        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
 
-        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
-        if include_pos(name) && id == command.id => elem_positions(range, set, body)
+        case XML.Elem(Markup(name, Position.Reported(id, file, range)), body)
+        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
 
         case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)