equal
deleted
inserted
replaced
25 |
25 |
26 /* file-system operations */ |
26 /* file-system operations */ |
27 |
27 |
28 def append(dir: String, source_path: Path): String = |
28 def append(dir: String, source_path: Path): String = |
29 (Path.explode(dir) + source_path).expand.implode |
29 (Path.explode(dir) + source_path).expand.implode |
30 |
|
31 def append_file(dir: String, raw_name: String): String = |
|
32 if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name)) |
|
33 else raw_name |
|
34 |
|
35 |
30 |
36 |
31 |
37 /* source files of Isabelle/ML bootstrap */ |
32 /* source files of Isabelle/ML bootstrap */ |
38 |
33 |
39 def source_file(raw_name: String): Option[String] = |
34 def source_file(raw_name: String): Option[String] = |