equal
deleted
inserted
replaced
357 : (List[Command.Blob], Int) = |
357 : (List[Command.Blob], Int) = |
358 { |
358 { |
359 val (files, index) = span_files(syntax, span) |
359 val (files, index) = span_files(syntax, span) |
360 val blobs = |
360 val blobs = |
361 files.map(file => |
361 files.map(file => |
362 Exn.capture { |
362 (Exn.capture { |
363 val name = |
363 val name = |
364 Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file))) |
364 Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file))) |
365 val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk))) |
365 val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk))) |
366 (name, blob) |
366 (name, blob) |
367 }) |
367 }).user_error) |
368 (blobs, index) |
368 (blobs, index) |
369 } |
369 } |
370 } |
370 } |
371 |
371 |
372 |
372 |