author | wenzelm |
Tue, 21 Apr 2020 22:19:59 +0200 | |
changeset 71777 | 3875815f5967 |
parent 71726 | a5fda30edae2 |
child 72375 | e48d93811ed7 |
permissions | -rw-r--r-- |
64188 | 1 |
/* Title: Pure/Admin/other_isabelle.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Manage other Isabelle distributions. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
67045 | 10 |
object Other_Isabelle |
11 |
{ |
|
12 |
def apply(isabelle_home: Path, |
|
67046 | 13 |
isabelle_identifier: String = "", |
14 |
user_home: Path = Path.explode("$USER_HOME"), |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
15 |
progress: Progress = new Progress): Other_Isabelle = |
69408
fb26935838c7
more robust, notably for macos /var vs. /private/var;
wenzelm
parents:
69404
diff
changeset
|
16 |
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress) |
67045 | 17 |
} |
18 |
||
19 |
class Other_Isabelle( |
|
20 |
val isabelle_home: Path, |
|
21 |
val isabelle_identifier: String, |
|
67046 | 22 |
user_home: Path, |
67045 | 23 |
progress: Progress) |
64188 | 24 |
{ |
25 |
other_isabelle => |
|
26 |
||
69404
de88761edbe2
clarified absolute isabelle_home and (implicitly) isabelle_home_user;
wenzelm
parents:
69401
diff
changeset
|
27 |
override def toString: String = isabelle_home.toString |
67046 | 28 |
|
29 |
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) |
|
30 |
error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT") |
|
31 |
||
64188 | 32 |
|
33 |
/* static system */ |
|
34 |
||
65930 | 35 |
def bash( |
36 |
script: String, |
|
37 |
redirect: Boolean = false, |
|
38 |
echo: Boolean = false, |
|
39 |
strict: Boolean = true): Process_Result = |
|
67046 | 40 |
progress.bash( |
41 |
"export USER_HOME=" + File.bash_path(user_home) + "\n" + |
|
42 |
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script, |
|
65930 | 43 |
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict) |
64188 | 44 |
|
65930 | 45 |
def apply( |
46 |
cmdline: String, |
|
47 |
redirect: Boolean = false, |
|
48 |
echo: Boolean = false, |
|
49 |
strict: Boolean = true): Process_Result = |
|
50 |
bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict) |
|
64188 | 51 |
|
52 |
def resolve_components(echo: Boolean): Unit = |
|
53 |
other_isabelle("components -a", redirect = true, echo = echo).check |
|
54 |
||
69166 | 55 |
def getenv(name: String): String = |
56 |
other_isabelle("getenv -b " + Bash.string(name)).check.out |
|
57 |
||
58 |
val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER")) |
|
64188 | 59 |
|
68754 | 60 |
val etc: Path = isabelle_home_user + Path.explode("etc") |
61 |
val etc_settings: Path = etc + Path.explode("settings") |
|
62 |
val etc_preferences: Path = etc + Path.explode("preferences") |
|
64188 | 63 |
|
69360 | 64 |
def copy_fonts(target_dir: Path): Unit = |
71601 | 65 |
Isabelle_Fonts.make_entries(getenv = getenv, hidden = true). |
69360 | 66 |
foreach(entry => File.copy(entry.path, target_dir)) |
64188 | 67 |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
68 |
|
69388 | 69 |
/* components */ |
70 |
||
71 |
def init_components( |
|
69434 | 72 |
components_base: Path = Components.default_components_base, |
69396 | 73 |
catalogs: List[String] = Nil, |
74 |
components: List[String] = Nil): List[String] = |
|
69388 | 75 |
{ |
69404
de88761edbe2
clarified absolute isabelle_home and (implicitly) isabelle_home_user;
wenzelm
parents:
69401
diff
changeset
|
76 |
val dir = Components.admin(isabelle_home) |
69396 | 77 |
catalogs.map(name => |
69434 | 78 |
"init_components " + File.bash_path(components_base) + " " + |
79 |
File.bash_path(dir + Path.basic(name))) ::: |
|
69396 | 80 |
components.map(name => |
69434 | 81 |
"init_component " + File.bash_path(components_base + Path.basic(name))) |
69388 | 82 |
} |
83 |
||
84 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
85 |
/* settings */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
86 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
87 |
def clean_settings(): Boolean = |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
88 |
if (!etc_settings.is_file) true |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
89 |
else if (File.read(etc_settings).startsWith("# generated by Isabelle")) { |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
90 |
etc_settings.file.delete; true |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
91 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
92 |
else false |
64188 | 93 |
|
69388 | 94 |
def init_settings(settings: List[String]) |
64188 | 95 |
{ |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
96 |
if (!clean_settings()) |
64188 | 97 |
error("Cannot proceed with existing user settings file: " + etc_settings) |
98 |
||
99 |
Isabelle_System.mkdirs(etc_settings.dir) |
|
100 |
File.write(etc_settings, |
|
101 |
"# generated by Isabelle " + Date.now() + "\n" + |
|
69388 | 102 |
"#-*- shell-script -*- :mode=shellscript:\n" + |
103 |
settings.mkString("\n", "\n", "\n")) |
|
64188 | 104 |
} |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
105 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
106 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
107 |
/* cleanup */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
108 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
109 |
def cleanup() |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
110 |
{ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
111 |
clean_settings() |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
112 |
etc.file.delete |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
113 |
isabelle_home_user.file.delete |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
114 |
} |
64188 | 115 |
} |