equal
deleted
inserted
replaced
15 options: Options, |
15 options: Options, |
16 progress: Progress, |
16 progress: Progress, |
17 deps: Sessions.Deps, |
17 deps: Sessions.Deps, |
18 output_dir: Path, |
18 output_dir: Path, |
19 node_name: Document.Node.Name, |
19 node_name: Document.Node.Name, |
20 node_status: Protocol.Node_Status, |
20 node_status: Document_Status.Node_Status, |
21 snapshot: Document.Snapshot) |
21 snapshot: Document.Snapshot) |
22 { |
22 { |
23 def write(file_name: Path, bytes: Bytes) |
23 def write(file_name: Path, bytes: Bytes) |
24 { |
24 { |
25 val path = output_dir + Path.basic(node_name.theory) + file_name |
25 val path = output_dir + Path.basic(node_name.theory) + file_name |