equal
deleted
inserted
replaced
44 def append(dir: String, source_path: Path): String = |
44 def append(dir: String, source_path: Path): String = |
45 (Path.explode(dir) + source_path).expand.implode |
45 (Path.explode(dir) + source_path).expand.implode |
46 |
46 |
47 def append_file(dir: String, raw_name: String): String = |
47 def append_file(dir: String, raw_name: String): String = |
48 if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name)) |
48 if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name)) |
49 else raw_name |
|
50 |
|
51 def append_file_url(dir: String, raw_name: String): String = |
|
52 if (Path.is_valid(raw_name)) "file://" + append(dir, Path.explode(raw_name)) |
|
53 else raw_name |
49 else raw_name |
54 |
50 |
55 |
51 |
56 |
52 |
57 /* source files of Isabelle/ML bootstrap */ |
53 /* source files of Isabelle/ML bootstrap */ |