27919
|
1 |
/* Title: Pure/Tools/isabelle_system.scala
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
27936
|
5 |
Isabelle system support: settings and path specifications.
|
27919
|
6 |
*/
|
|
7 |
|
|
8 |
package isabelle
|
|
9 |
|
27936
|
10 |
import java.util.regex.{Pattern, Matcher}
|
|
11 |
import java.io.File
|
|
12 |
|
27919
|
13 |
|
|
14 |
object IsabelleSystem {
|
|
15 |
|
|
16 |
/* Isabelle settings */
|
|
17 |
|
27953
|
18 |
def getenv(name: String) = {
|
|
19 |
val value = System.getenv(name)
|
|
20 |
if (value != null) value else ""
|
|
21 |
}
|
27919
|
22 |
|
27956
|
23 |
class BadVariable(val name: String) extends Exception {
|
|
24 |
override def toString = "BadVariable: " + name
|
|
25 |
}
|
27953
|
26 |
|
|
27 |
def getenv_strict(name: String) = {
|
|
28 |
val value = getenv(name)
|
|
29 |
if (value != "") value else throw new BadVariable(name)
|
27919
|
30 |
}
|
|
31 |
|
27936
|
32 |
|
|
33 |
/* File path specifications */
|
|
34 |
|
|
35 |
private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")
|
|
36 |
|
|
37 |
def platform_path(source_path: String) = {
|
|
38 |
val result_path = new StringBuilder
|
27919
|
39 |
|
27936
|
40 |
def init(path: String) = {
|
|
41 |
val cygdrive = cygdrive_pattern.matcher(path)
|
|
42 |
if (cygdrive.matches) {
|
27953
|
43 |
result_path.length = 0
|
27936
|
44 |
result_path.append(cygdrive.group(1))
|
|
45 |
result_path.append(":")
|
|
46 |
result_path.append(File.separator)
|
|
47 |
cygdrive.group(2)
|
|
48 |
}
|
|
49 |
else if (path.startsWith("/")) {
|
27953
|
50 |
result_path.length = 0
|
|
51 |
result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
|
27936
|
52 |
path.substring(1)
|
|
53 |
}
|
|
54 |
else path
|
|
55 |
}
|
|
56 |
def append(path: String) = {
|
|
57 |
for (p <- init(path).split("/")) {
|
|
58 |
if (p != "") {
|
|
59 |
val len = result_path.length
|
|
60 |
if (len > 0 && result_path(len - 1) != File.separatorChar)
|
|
61 |
result_path.append(File.separator)
|
|
62 |
result_path.append(p)
|
|
63 |
}
|
|
64 |
}
|
|
65 |
}
|
|
66 |
for (p <- init(source_path).split("/")) {
|
27953
|
67 |
if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
|
|
68 |
else if (p == "~") append(getenv_strict("HOME"))
|
|
69 |
else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
|
27936
|
70 |
else append(p)
|
|
71 |
}
|
|
72 |
result_path.toString
|
|
73 |
}
|
27953
|
74 |
|
|
75 |
|
|
76 |
/* Cygwin shell prefix */
|
|
77 |
|
|
78 |
def shell_prefix() = {
|
|
79 |
if (Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM")))
|
27962
|
80 |
Some(platform_path("/bin/env"))
|
27953
|
81 |
else None
|
|
82 |
}
|
|
83 |
|
27919
|
84 |
}
|