equal
deleted
inserted
replaced
90 handle ERROR msg => error (msg ^ Position.here pos); |
90 handle ERROR msg => error (msg ^ Position.here pos); |
91 fun make_file src_path (Exn.Res (file_node, NONE)) = |
91 fun make_file src_path (Exn.Res (file_node, NONE)) = |
92 Exn.interruptible_capture (fn () => |
92 Exn.interruptible_capture (fn () => |
93 read_file_node file_node master_dir pos src_path) () |
93 read_file_node file_node master_dir pos src_path) () |
94 | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) = |
94 | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) = |
95 Exn.Res (blob_file src_path lines digest file_node) |
95 (Position.report pos Markup.language_path; |
|
96 Exn.Res (blob_file src_path lines digest file_node)) |
96 | make_file _ (Exn.Exn e) = Exn.Exn e; |
97 | make_file _ (Exn.Exn e) = Exn.Exn e; |
97 val src_paths = Keyword.command_files keywords cmd path; |
98 val src_paths = Keyword.command_files keywords cmd path; |
98 val files = |
99 val files = |
99 if null blobs then |
100 if null blobs then |
100 map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) |
101 map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) |