clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
--- 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 =
--- 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