equal
deleted
inserted
replaced
37 |
37 |
38 |
38 |
39 /* file-system operations */ |
39 /* file-system operations */ |
40 |
40 |
41 def append(dir: String, source_path: Path): String = |
41 def append(dir: String, source_path: Path): String = |
42 (Path.explode(dir) + source_path).implode |
42 (Path.explode(dir) + source_path).expand.implode |
43 |
43 |
44 def read_header(name: Document.Node.Name): Thy_Header = |
44 def read_header(name: Document.Node.Name): Thy_Header = |
45 { |
45 { |
46 val file = new JFile(name.node) |
46 val file = new JFile(name.node) |
47 if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) |
47 if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) |