75 let |
75 let |
76 val source = Token.input_of tok; |
76 val source = Token.input_of tok; |
77 val pos = Input.pos_of source; |
77 val pos = Input.pos_of source; |
78 val delimited = Input.is_delimited source; |
78 val delimited = Input.is_delimited source; |
79 |
79 |
80 fun make_file (Exn.Res {file_node, src_path, content = NONE}) = |
80 fun make_file (Exn.Res {file_node, src_path, content}) = |
81 Exn.interruptible_capture (fn () => |
81 let val _ = Position.report pos (Markup.language_path delimited) in |
82 Resources.read_file_node file_node master_dir pos delimited src_path) () |
82 case content of |
83 | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) = |
83 NONE => |
84 (Position.report pos (Markup.language_path delimited); |
84 Exn.interruptible_capture (fn () => |
85 Exn.Res (blob_file src_path lines digest file_node)) |
85 Resources.read_file_node file_node master_dir (src_path, pos)) () |
|
86 | SOME (digest, lines) => Exn.Res (blob_file src_path lines digest file_node) |
|
87 end |
86 | make_file (Exn.Exn e) = Exn.Exn e; |
88 | make_file (Exn.Exn e) = Exn.Exn e; |
87 val files = map make_file blobs; |
89 val files = map make_file blobs; |
88 in |
90 in |
89 toks |> map_index (fn (i, tok) => |
91 toks |> map_index (fn (i, tok) => |
90 if i = blobs_index then Token.put_files files tok else tok) |
92 if i = blobs_index then Token.put_files files tok else tok) |