# HG changeset patch
# User wenzelm
# Date 1428830616 -7200
# Node ID c42d65e11b6e8bd42c5b4a133572e4f3e4a3b91a
# Parent  d84b355f341fa52c9e76316a5bf65a9683fb17fe
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;

diff -r d84b355f341f -r c42d65e11b6e src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Apr 12 00:26:24 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Apr 12 11:23:36 2015 +0200
@@ -92,7 +92,8 @@
                   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))) =
-                  Exn.Res (blob_file src_path lines digest file_node)
+                  (Position.report pos Markup.language_path;
+                    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;
             val files =
diff -r d84b355f341f -r c42d65e11b6e src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Apr 12 00:26:24 2015 +0200
+++ b/src/Pure/PIDE/document.ML	Sun Apr 12 11:23:36 2015 +0200
@@ -388,10 +388,8 @@
                     map_filter Exn.get_exn blobs_digests
                     |> List.app (Output.error_message o Runtime.exn_message)
                   else (*auxiliary files*)
-                    let val pos = Token.pos_of (nth tokens blobs_index) in
-                      Position.reports
-                        ((pos, Markup.language_path) :: maps (blob_reports pos) blobs_digests)
-                    end;
+                    let val pos = Token.pos_of (nth tokens blobs_index)
+                    in Position.reports (maps (blob_reports pos) blobs_digests) end;
               in tokens end) ());
       val commands' =
         Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands