author | wenzelm |
Mon, 03 Dec 2018 22:07:23 +0100 | |
changeset 69398 | 0698ded5caf1 |
parent 69395 | d1c4a1dee9e7 |
child 69401 | 7a1b7b737c02 |
permissions | -rw-r--r-- |
69395 | 1 |
/* Title: Pure/Admin/components.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Isabelle system components. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Components |
|
11 |
{ |
|
12 |
/* component collections */ |
|
13 |
||
14 |
def admin(dir: Path): Path = dir + Path.explode("Admin/components") |
|
15 |
||
16 |
def contrib(dir: Path = Path.current, name: String = ""): Path = |
|
17 |
dir + Path.explode("contrib") + Path.explode(name) |
|
18 |
||
69398
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
19 |
def download(dir: Path, names: List[String], progress: Progress = No_Progress) |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
20 |
{ |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
21 |
Isabelle_System.mkdirs(dir) |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
22 |
for (name <- names) { |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
23 |
val archive = name + ".tar.gz" |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
24 |
val target = dir + Path.explode(archive) |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
25 |
if (!target.is_file) { |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
26 |
val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
27 |
progress.echo("Getting " + quote(remote)) |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
28 |
Bytes.write(target, Url.read_bytes(Url(remote))) |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
29 |
} |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
30 |
} |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
31 |
} |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
32 |
|
69395 | 33 |
|
34 |
/* component directory content */ |
|
35 |
||
36 |
def settings(dir: Path): Path = dir + Path.explode("etc/settings") |
|
37 |
def components(dir: Path): Path = dir + Path.explode("etc/components") |
|
38 |
||
39 |
def check_dir(dir: Path): Boolean = |
|
40 |
settings(dir).is_file || components(dir).is_file |
|
41 |
||
42 |
def read_components(dir: Path): List[String] = |
|
43 |
split_lines(File.read(components(dir))).filter(_.nonEmpty) |
|
44 |
||
45 |
def write_components(dir: Path, lines: List[String]): Unit = |
|
46 |
File.write(components(dir), terminate_lines(lines)) |
|
47 |
} |