author | wenzelm |
Thu, 04 Jun 2009 22:01:54 +0200 | |
changeset 31436 | dde1b4d1c95b |
parent 31234 | 6ce6801129de |
child 31443 | c23663825e23 |
permissions | -rw-r--r-- |
30175 | 1 |
/* Title: Pure/System/isabelle_system.scala |
27919 | 2 |
Author: Makarius |
3 |
||
27974 | 4 |
Isabelle system support -- basic Cygwin/Posix compatibility. |
27919 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
27936 | 9 |
import java.util.regex.{Pattern, Matcher} |
28063 | 10 |
import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException} |
11 |
||
12 |
import scala.io.Source |
|
27936 | 13 |
|
27919 | 14 |
|
29174 | 15 |
class IsabelleSystem { |
27919 | 16 |
|
28057 | 17 |
val charset = "UTF-8" |
18 |
||
19 |
||
28046 | 20 |
/* Isabelle environment settings */ |
27919 | 21 |
|
29177 | 22 |
private val environment = System.getenv |
23 |
||
27953 | 24 |
def getenv(name: String) = { |
29177 | 25 |
val value = environment.get(if (name == "HOME") "HOME_JVM" else name) |
27953 | 26 |
if (value != null) value else "" |
27 |
} |
|
27919 | 28 |
|
27953 | 29 |
def getenv_strict(name: String) = { |
31234
6ce6801129de
getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);
wenzelm
parents:
30175
diff
changeset
|
30 |
val value = getenv(name) |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27974
diff
changeset
|
31 |
if (value != "") value else error("Undefined environment variable: " + name) |
27919 | 32 |
} |
33 |
||
29177 | 34 |
val is_cygwin = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM")) |
28046 | 35 |
|
27936 | 36 |
|
27974 | 37 |
/* file path specifications */ |
27936 | 38 |
|
39 |
private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)") |
|
40 |
||
41 |
def platform_path(source_path: String) = { |
|
42 |
val result_path = new StringBuilder |
|
27919 | 43 |
|
27936 | 44 |
def init(path: String) = { |
45 |
val cygdrive = cygdrive_pattern.matcher(path) |
|
46 |
if (cygdrive.matches) { |
|
27953 | 47 |
result_path.length = 0 |
27936 | 48 |
result_path.append(cygdrive.group(1)) |
49 |
result_path.append(":") |
|
50 |
result_path.append(File.separator) |
|
51 |
cygdrive.group(2) |
|
52 |
} |
|
53 |
else if (path.startsWith("/")) { |
|
27953 | 54 |
result_path.length = 0 |
55 |
result_path.append(getenv_strict("ISABELLE_ROOT_JVM")) |
|
27936 | 56 |
path.substring(1) |
57 |
} |
|
58 |
else path |
|
59 |
} |
|
60 |
def append(path: String) = { |
|
61 |
for (p <- init(path).split("/")) { |
|
62 |
if (p != "") { |
|
63 |
val len = result_path.length |
|
64 |
if (len > 0 && result_path(len - 1) != File.separatorChar) |
|
65 |
result_path.append(File.separator) |
|
66 |
result_path.append(p) |
|
67 |
} |
|
68 |
} |
|
69 |
} |
|
70 |
for (p <- init(source_path).split("/")) { |
|
27953 | 71 |
if (p.startsWith("$")) append(getenv_strict(p.substring(1))) |
72 |
else if (p == "~") append(getenv_strict("HOME")) |
|
73 |
else if (p == "~~") append(getenv_strict("ISABELLE_HOME")) |
|
27936 | 74 |
else append(p) |
75 |
} |
|
76 |
result_path.toString |
|
77 |
} |
|
27953 | 78 |
|
29152 | 79 |
def platform_file(path: String) = |
80 |
new File(platform_path(path)) |
|
81 |
||
27953 | 82 |
|
31436 | 83 |
/* source files */ |
84 |
||
85 |
private def try_file(file: File) = if (file.isFile) Some(file) else None |
|
86 |
||
87 |
def source_file(path: String): Option[File] = { |
|
88 |
if (path == "ML") None |
|
89 |
else if (path.startsWith("/") || path == "") |
|
90 |
try_file(platform_file(path)) |
|
91 |
else { |
|
92 |
val pure_file = platform_file("~~/src/Pure/" + path) |
|
93 |
if (pure_file.isFile) Some(pure_file) |
|
94 |
else if (getenv("ML_SOURCES") != "") |
|
95 |
try_file(platform_file("$ML_SOURCES/" + path)) |
|
96 |
else None |
|
97 |
} |
|
98 |
} |
|
99 |
||
100 |
||
101 |
/* shell processes */ |
|
27953 | 102 |
|
29177 | 103 |
def execute(redirect: Boolean, args: String*): Process = { |
104 |
val cmdline = new java.util.LinkedList[String] |
|
105 |
if (is_cygwin) cmdline.add(platform_path("/bin/env")) |
|
106 |
for (s <- args) cmdline.add(s) |
|
27974 | 107 |
|
29177 | 108 |
val proc = new ProcessBuilder(cmdline) |
29180 | 109 |
proc.environment.clear |
110 |
proc.environment.putAll(environment) |
|
111 |
proc.redirectErrorStream(redirect) |
|
112 |
proc.start |
|
28046 | 113 |
} |
114 |
||
28063 | 115 |
|
116 |
/* Isabelle tools (non-interactive) */ |
|
117 |
||
28496
4cff10648928
renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents:
28063
diff
changeset
|
118 |
def isabelle_tool(args: String*) = { |
28063 | 119 |
val proc = |
29177 | 120 |
try { execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) } |
28063 | 121 |
catch { case e: IOException => error(e.getMessage) } |
122 |
proc.getOutputStream.close |
|
29174 | 123 |
val output = Source.fromInputStream(proc.getInputStream, charset).mkString |
28063 | 124 |
val rc = proc.waitFor |
125 |
(output, rc) |
|
126 |
} |
|
127 |
||
128 |
||
129 |
/* named pipes */ |
|
130 |
||
131 |
def mk_fifo() = { |
|
28496
4cff10648928
renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents:
28063
diff
changeset
|
132 |
val (result, rc) = isabelle_tool("mkfifo") |
28063 | 133 |
if (rc == 0) result.trim |
134 |
else error(result) |
|
135 |
} |
|
136 |
||
137 |
def rm_fifo(fifo: String) = { |
|
28496
4cff10648928
renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents:
28063
diff
changeset
|
138 |
val (result, rc) = isabelle_tool("rmfifo", fifo) |
28063 | 139 |
if (rc != 0) error(result) |
140 |
} |
|
141 |
||
29177 | 142 |
def fifo_reader(fifo: String) = { |
143 |
// blocks until writer is ready |
|
144 |
val stream = |
|
145 |
if (is_cygwin) execute(false, "cat", fifo).getInputStream |
|
146 |
else new FileInputStream(fifo) |
|
147 |
new BufferedReader(new InputStreamReader(stream, charset)) |
|
148 |
} |
|
28063 | 149 |
|
29152 | 150 |
|
151 |
/* find logics */ |
|
152 |
||
153 |
def find_logics() = { |
|
154 |
val ml_ident = getenv_strict("ML_IDENTIFIER") |
|
155 |
var logics: Set[String] = Set() |
|
156 |
for (dir <- getenv_strict("ISABELLE_PATH").split(":")) { |
|
157 |
val files = platform_file(dir + "/" + ml_ident).listFiles() |
|
158 |
if (files != null) { |
|
159 |
for (file <- files if file.isFile) logics += file.getName |
|
160 |
} |
|
161 |
} |
|
162 |
logics.toList.sort(_ < _) |
|
163 |
} |
|
29570 | 164 |
|
165 |
||
166 |
/* symbols */ |
|
167 |
||
168 |
private def read_symbols(path: String) = { |
|
169 |
val file = new File(platform_path(path)) |
|
31436 | 170 |
if (file.isFile) Source.fromFile(file).getLines |
29570 | 171 |
else Iterator.empty |
172 |
} |
|
173 |
val symbols = new Symbol.Interpretation( |
|
174 |
read_symbols("$ISABELLE_HOME/etc/symbols") ++ |
|
175 |
read_symbols("$ISABELLE_HOME_USER/etc/symbols")) |
|
27919 | 176 |
} |