equal
deleted
inserted
replaced
67 |
67 |
68 |
68 |
69 /* components */ |
69 /* components */ |
70 |
70 |
71 def init_components( |
71 def init_components( |
|
72 component_repository: String = Components.default_component_repository, |
72 components_base: Path = Components.default_components_base, |
73 components_base: Path = Components.default_components_base, |
73 catalogs: List[String] = Nil, |
74 catalogs: List[String] = Nil, |
74 components: List[String] = Nil): List[String] = |
75 components: List[String] = Nil): List[String] = |
75 { |
76 { |
76 val dir = Components.admin(isabelle_home) |
77 val dir = Components.admin(isabelle_home) |
|
78 |
|
79 ("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) :: |
77 catalogs.map(name => |
80 catalogs.map(name => |
78 "init_components " + File.bash_path(components_base) + " " + |
81 "init_components " + File.bash_path(components_base) + " " + |
79 File.bash_path(dir + Path.basic(name))) ::: |
82 File.bash_path(dir + Path.basic(name))) ::: |
80 components.map(name => |
83 components.map(name => |
81 "init_component " + File.bash_path(components_base + Path.basic(name))) |
84 "init_component " + File.bash_path(components_base + Path.basic(name))) |