--- a/src/Pure/PIDE/document.ML Sun Aug 28 14:44:34 2022 +0200
+++ b/src/Pure/PIDE/document.ML Sun Aug 28 14:55:40 2022 +0200
@@ -402,9 +402,6 @@
blob_digest |> Exn.map_res (fn {file_node, src_path, digest} =>
{file_node = file_node, src_path = src_path, content = Option.map (the_blob state) digest});
-fun blob_reports pos (blob_digest: blob_digest) =
- (case blob_digest of Exn.Res {file_node, ...} => [(pos, Markup.path file_node)] | _ => []);
-
(* commands *)
@@ -449,8 +446,11 @@
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 (maps (blob_reports pos) blobs_digests) end;
+ let
+ val pos = Token.pos_of (nth tokens blobs_index);
+ fun reports (Exn.Res {file_node, ...}) = [(pos, Markup.path file_node)]
+ | reports _ = [];
+ in Position.reports (maps reports blobs_digests) end;
in tokens end) ());
val commands' =
Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands