23 ) { |
23 ) { |
24 other_isabelle => |
24 other_isabelle => |
25 |
25 |
26 override def toString: String = isabelle_home.toString |
26 override def toString: String = isabelle_home.toString |
27 |
27 |
28 if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) |
28 if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { |
29 error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT") |
29 error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT") |
|
30 } |
30 |
31 |
31 |
32 |
32 /* static system */ |
33 /* static system */ |
33 |
34 |
34 def bash( |
35 def bash( |
35 script: String, |
36 script: String, |
36 redirect: Boolean = false, |
37 redirect: Boolean = false, |
37 echo: Boolean = false, |
38 echo: Boolean = false, |
38 strict: Boolean = true): Process_Result = |
39 strict: Boolean = true |
|
40 ): Process_Result = { |
39 progress.bash( |
41 progress.bash( |
40 "export USER_HOME=" + File.bash_path(user_home) + "\n" + |
42 "export USER_HOME=" + File.bash_path(user_home) + "\n" + |
41 Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script, |
43 Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script, |
42 env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict) |
44 env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict) |
|
45 } |
43 |
46 |
44 def apply( |
47 def apply( |
45 cmdline: String, |
48 cmdline: String, |
46 redirect: Boolean = false, |
49 redirect: Boolean = false, |
47 echo: Boolean = false, |
50 echo: Boolean = false, |
48 strict: Boolean = true): Process_Result = |
51 strict: Boolean = true |
|
52 ): Process_Result = { |
49 bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict) |
53 bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict) |
|
54 } |
50 |
55 |
51 def resolve_components(echo: Boolean): Unit = |
56 def resolve_components(echo: Boolean): Unit = { |
52 other_isabelle( |
57 other_isabelle( |
53 "env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) + |
58 "env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) + |
54 " isabelle components -a", redirect = true, echo = echo).check |
59 " isabelle components -a", redirect = true, echo = echo).check |
|
60 } |
55 |
61 |
56 def getenv(name: String): String = |
62 def getenv(name: String): String = |
57 other_isabelle("getenv -b " + Bash.string(name)).check.out |
63 other_isabelle("getenv -b " + Bash.string(name)).check.out |
58 |
64 |
59 val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER")) |
65 val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER")) |
85 /* settings */ |
91 /* settings */ |
86 |
92 |
87 def clean_settings(): Boolean = |
93 def clean_settings(): Boolean = |
88 if (!etc_settings.is_file) true |
94 if (!etc_settings.is_file) true |
89 else if (File.read(etc_settings).startsWith("# generated by Isabelle")) { |
95 else if (File.read(etc_settings).startsWith("# generated by Isabelle")) { |
90 etc_settings.file.delete; true |
96 etc_settings.file.delete |
|
97 true |
91 } |
98 } |
92 else false |
99 else false |
93 |
100 |
94 def init_settings(settings: List[String]): Unit = { |
101 def init_settings(settings: List[String]): Unit = { |
95 if (!clean_settings()) |
102 if (!clean_settings()) { |
96 error("Cannot proceed with existing user settings file: " + etc_settings) |
103 error("Cannot proceed with existing user settings file: " + etc_settings) |
|
104 } |
97 |
105 |
98 Isabelle_System.make_directory(etc_settings.dir) |
106 Isabelle_System.make_directory(etc_settings.dir) |
99 File.write(etc_settings, |
107 File.write(etc_settings, |
100 "# generated by Isabelle " + Date.now() + "\n" + |
108 "# generated by Isabelle " + Date.now() + "\n" + |
101 "#-*- shell-script -*- :mode=shellscript:\n" + |
109 "#-*- shell-script -*- :mode=shellscript:\n" + |