equal
deleted
inserted
replaced
13 |
13 |
14 object IsabelleSystem { |
14 object IsabelleSystem { |
15 |
15 |
16 /* Isabelle settings */ |
16 /* Isabelle settings */ |
17 |
17 |
18 class BadSetting(val name: String) extends Exception |
18 def getenv(name: String) = { |
|
19 val value = System.getenv(name) |
|
20 if (value != null) value else "" |
|
21 } |
19 |
22 |
20 def get_setting(name: String) = { |
23 class BadVariable(val name: String) extends Exception |
21 val value = System.getenv(name) |
24 |
22 if (value == null || value == "") throw new BadSetting(name) |
25 def getenv_strict(name: String) = { |
23 else value |
26 val value = getenv(name) |
|
27 if (value != "") value else throw new BadVariable(name) |
24 } |
28 } |
25 |
29 |
26 |
30 |
27 /* File path specifications */ |
31 /* File path specifications */ |
28 |
32 |
32 val result_path = new StringBuilder |
36 val result_path = new StringBuilder |
33 |
37 |
34 def init(path: String) = { |
38 def init(path: String) = { |
35 val cygdrive = cygdrive_pattern.matcher(path) |
39 val cygdrive = cygdrive_pattern.matcher(path) |
36 if (cygdrive.matches) { |
40 if (cygdrive.matches) { |
37 result_path.setLength(0) |
41 result_path.length = 0 |
38 result_path.append(cygdrive.group(1)) |
42 result_path.append(cygdrive.group(1)) |
39 result_path.append(":") |
43 result_path.append(":") |
40 result_path.append(File.separator) |
44 result_path.append(File.separator) |
41 cygdrive.group(2) |
45 cygdrive.group(2) |
42 } |
46 } |
43 else if (path.startsWith("/")) { |
47 else if (path.startsWith("/")) { |
44 result_path.setLength(0) |
48 result_path.length = 0 |
45 result_path.append(get_setting("ISABELLE_ROOT_JVM")) |
49 result_path.append(getenv_strict("ISABELLE_ROOT_JVM")) |
46 path.substring(1) |
50 path.substring(1) |
47 } |
51 } |
48 else path |
52 else path |
49 } |
53 } |
50 def append(path: String) = { |
54 def append(path: String) = { |
56 result_path.append(p) |
60 result_path.append(p) |
57 } |
61 } |
58 } |
62 } |
59 } |
63 } |
60 for (p <- init(source_path).split("/")) { |
64 for (p <- init(source_path).split("/")) { |
61 if (p.startsWith("$")) append(get_setting(p.substring(1))) |
65 if (p.startsWith("$")) append(getenv_strict(p.substring(1))) |
62 else if (p == "~") append(get_setting("HOME")) |
66 else if (p == "~") append(getenv_strict("HOME")) |
63 else if (p == "~~") append(get_setting("ISABELLE_HOME")) |
67 else if (p == "~~") append(getenv_strict("ISABELLE_HOME")) |
64 else append(p) |
68 else append(p) |
65 } |
69 } |
66 result_path.toString |
70 result_path.toString |
67 } |
71 } |
|
72 |
|
73 |
|
74 /* Cygwin shell prefix */ |
|
75 |
|
76 def shell_prefix() = { |
|
77 if (Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))) |
|
78 Some(platform_path("/usr/bin/env")) |
|
79 else None |
|
80 } |
|
81 |
68 } |
82 } |