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 components_base(base: Option[Path]): Path = |
|
72 base getOrElse Components.contrib(isabelle_home_user.absolute.dir) |
|
73 |
71 def init_components( |
74 def init_components( |
72 base: Option[Path] = None, |
75 base: Option[Path] = None, |
73 catalogs: List[String] = Nil, |
76 catalogs: List[String] = Nil, |
74 components: List[String] = Nil): List[String] = |
77 components: List[String] = Nil): List[String] = |
75 { |
78 { |
76 val base_dir = base getOrElse Components.contrib(isabelle_home_user.absolute.dir) |
79 val base_dir = components_base(base) |
77 val dir = Components.admin(isabelle_home.absolute) |
80 val dir = Components.admin(isabelle_home.absolute) |
78 catalogs.map(name => |
81 catalogs.map(name => |
79 "init_components " + File.bash_path(base_dir) + " " + File.bash_path(dir + Path.basic(name))) ::: |
82 "init_components " + File.bash_path(base_dir) + " " + File.bash_path(dir + Path.basic(name))) ::: |
80 components.map(name => |
83 components.map(name => |
81 "init_component " + File.bash_path(base_dir + Path.basic(name))) |
84 "init_component " + File.bash_path(base_dir + Path.basic(name))) |