equal
deleted
inserted
replaced
66 foreach(entry => File.copy(entry.path, target_dir)) |
66 foreach(entry => File.copy(entry.path, target_dir)) |
67 |
67 |
68 |
68 |
69 /* components */ |
69 /* components */ |
70 |
70 |
71 def default_components_base: Path = isabelle_home_user.absolute.dir + Path.explode("contrib") |
71 def default_components_base: Path = Components.contrib(isabelle_home_user.absolute.dir) |
72 def default_components_dir: Path = isabelle_home.absolute + Path.explode("Admin/components") |
72 def default_components_dir: Path = Components.admin(isabelle_home.absolute) |
73 def default_catalogs: List[String] = List("main") |
73 def default_catalogs: List[String] = List("main") |
74 |
74 |
75 def init_components( |
75 def init_components( |
76 base: Path = default_components_base, |
76 base: Path = default_components_base, |
77 dir: Path = default_components_dir, |
77 dir: Path = default_components_dir, |