clarified markup for embedded files, early before execution;

--- a/src/Pure/PIDE/command.ML	Thu Mar 12 20:34:08 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Mar 12 22:00:51 2015 +0100
@@ -51,21 +51,19 @@
 
 fun read_file_node file_node master_dir pos src_path =
   let
-    val _ = Position.report pos Markup.language_path;
     val _ =
       (case try Url.explode file_node of
         NONE => ()
       | SOME (Url.File _) => ()
       | _ =>
-         (Position.report pos (Markup.path file_node);
           error ("Prover cannot load remote file " ^
-            Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
+            Markup.markup (Markup.path file_node) (quote file_node)));
     val full_path = File.check_file (File.full_path master_dir src_path);
-    val _ = Position.report pos (Markup.path (Path.implode full_path));
     val text = File.read full_path;
     val lines = split_lines text;
     val digest = SHA1.digest text;
-  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
+  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
+  handle ERROR msg => error (msg ^ Position.here pos);
 
 val read_file = read_file_node "";
 
@@ -89,8 +87,7 @@
                 Exn.interruptible_capture (fn () =>
                   read_file_node file_node master_dir pos src_path) ()
             | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
-               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
-                Exn.Res (blob_file src_path lines digest file_node))
+                Exn.Res (blob_file src_path lines digest file_node)
             | make_file _ (Exn.Exn e) = Exn.Exn e;
           val src_paths = Keyword.command_files keywords cmd path;
         in

--- a/src/Pure/PIDE/document.ML	Thu Mar 12 20:34:08 2015 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 12 22:00:51 2015 +0100
@@ -19,7 +19,7 @@
   val init_state: state
   val define_blob: string -> string -> state -> state
   type blob_digest = (string * string option) Exn.result
-  val define_command: Document_ID.command -> string -> blob_digest list ->
+  val define_command: Document_ID.command -> string -> blob_digest list -> int ->
     ((int * int) * string) list -> state -> state
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
@@ -359,23 +359,37 @@
   blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
     (file_node, Option.map (the_blob state) raw_digest));
 
+fun blob_reports pos (blob_digest: blob_digest) =
+  (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []);
+
 
 (* commands *)
 
-fun define_command command_id name command_blobs toks =
+fun define_command command_id name command_blobs blobs_index toks =
   map_state (fn (versions, blobs, commands, execution) =>
     let
       val id = Document_ID.print command_id;
       val span =
         Lazy.lazy (fn () =>
           Position.setmp_thread_data (Position.id_only id)
-            (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
+            (fn () =>
+              let
+                val (tokens, _) = fold_map Token.make toks (Position.id id);
+                val _ =
+                  (case try (Token.pos_of o nth tokens) blobs_index of
+                    SOME pos =>
+                      if Position.is_reported pos then
+                        Position.reports
+                          ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
+                      else ()
+                  | NONE => ());
+              in tokens end) ());
+      val commands' =
+        Inttab.update_new (command_id, (name, command_blobs, span)) commands
+          handle Inttab.DUP dup => err_dup "command" dup;
       val _ =
         Position.setmp_thread_data (Position.id_only id)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
-      val commands' =
-        Inttab.update_new (command_id, (name, command_blobs, span)) commands
-          handle Inttab.DUP dup => err_dup "command" dup;
     in (versions, blobs, commands', execution) end);
 
 fun the_command (State {commands, ...}) command_id =

--- a/src/Pure/PIDE/protocol.ML	Thu Mar 12 20:34:08 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Mar 12 22:00:51 2015 +0100
@@ -30,17 +30,20 @@
   Isabelle_Process.protocol_command "Document.define_command"
     (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
       let
-        val blobs =
+        val (blobs, blobs_index) =
           YXML.parse_body blobs_yxml |>
             let open XML.Decode in
-              list (variant
-               [fn ([], a) => Exn.Res (pair string (option string) a),
-                fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))])
+              pair
+                (list (variant
+                 [fn ([], a) => Exn.Res (pair string (option string) a),
+                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
+                int
             end;
         val toks =
           (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
       in
-        Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
+        Document.change_state
+          (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
       end);
 
 val _ =

--- a/src/Pure/PIDE/protocol.scala	Thu Mar 12 20:34:08 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Mar 12 22:00:51 2015 +0100
@@ -392,7 +392,7 @@
               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
 
-      YXML.string_of_body(list(encode_blob)(command.blobs))
+      YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     }
 
     val toks = command.span.content