author | wenzelm |
Sun, 06 Jan 2008 16:36:29 +0100 | |
changeset 25850 | dfca7b555e5c |
parent 25837 | 2a7efcfe9b54 |
child 26592 | 44cc22b19330 |
permissions | -rw-r--r-- |
25648 | 1 |
/* |
2 |
* $Id$ |
|
3 |
*/ |
|
4 |
||
5 |
package isabelle; |
|
6 |
||
7 |
import java.io.*; |
|
25791 | 8 |
import java.util.Locale; |
25658
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
9 |
import java.util.ArrayList; |
25791 | 10 |
import java.util.Properties; |
11 |
import java.util.Enumeration; |
|
25648 | 12 |
import java.util.concurrent.LinkedBlockingQueue; |
13 |
||
25745 | 14 |
/** |
15 |
* Posix process wrapper for Isabelle (see also <code>src/Pure/Tools/isabelle_process.ML</code>). |
|
16 |
* <p> |
|
25791 | 17 |
* |
25745 | 18 |
* The process model: |
19 |
* <p> |
|
20 |
* |
|
21 |
* <ol> |
|
22 |
* <li> input |
|
23 |
* <ul> |
|
24 |
* <li> stdin stream |
|
25 |
* <li> signals (interrupt, kill) |
|
26 |
* </ul> |
|
27 |
* |
|
28 |
* <li> output/results |
|
29 |
* <ul> |
|
30 |
* <li> stdout stream, interspersed with marked Isabelle messages |
|
31 |
* <li> stderr stream |
|
25837
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
32 |
* <li> process init (pid and session property) |
25745 | 33 |
* <li> process exit (return code) |
34 |
* </ul> |
|
35 |
* </ol> |
|
25791 | 36 |
* |
25745 | 37 |
* I/O is fully asynchronous, with unrestricted buffers. Text is encoded as UTF-8. |
38 |
* <p> |
|
25791 | 39 |
* |
25745 | 40 |
* System properties: |
41 |
* <p> |
|
25791 | 42 |
* |
25745 | 43 |
* <dl> |
44 |
* <dt> <code>isabelle.home</code> <di> <code>ISABELLE_HOME</code> of Isabelle installation |
|
45 |
* (default determined from isabelle-process via <code>PATH</code>) |
|
46 |
* <dt> <code>isabelle.shell</code> <di> optional shell command for <code>isabelle-process</code> (also requires isabelle.home) |
|
47 |
* <dt> <code>isabelle.kill</code> <di> optional kill command (default <code>kill</code>) |
|
48 |
*/ |
|
49 |
||
25648 | 50 |
public class IsabelleProcess { |
51 |
private volatile Process proc = null; |
|
52 |
private volatile String pid = null; |
|
53 |
private volatile boolean closing = false; |
|
54 |
private LinkedBlockingQueue<String> output = null; |
|
55 |
||
25837
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
56 |
public volatile String session = null; |
25648 | 57 |
|
25837
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
58 |
|
25745 | 59 |
/** |
60 |
* Models failures in process management. |
|
61 |
*/ |
|
25648 | 62 |
public static class IsabelleProcessException extends Exception { |
63 |
public IsabelleProcessException() { |
|
64 |
super(); |
|
65 |
} |
|
66 |
public IsabelleProcessException(String msg) { |
|
67 |
super(msg); |
|
68 |
} |
|
69 |
}; |
|
70 |
||
71 |
||
25745 | 72 |
/** |
73 |
* Models cooked results from the process. |
|
74 |
*/ |
|
25648 | 75 |
public static class Result { |
76 |
public enum Kind { |
|
25837
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
77 |
STDIN, STDOUT, STDERR, SIGNAL, EXIT, // Posix channels/events |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
78 |
WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT, INIT, // Isabelle messages |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
79 |
SYSTEM // internal system notification |
25648 | 80 |
}; |
81 |
public Kind kind; |
|
25807 | 82 |
public Properties props; |
25648 | 83 |
public String result; |
84 |
||
25807 | 85 |
public Result(Kind kind, Properties props, String result) { |
25648 | 86 |
this.kind = kind; |
25807 | 87 |
this.props = props; |
25648 | 88 |
this.result = result; |
89 |
} |
|
90 |
||
25747 | 91 |
public boolean isRaw() { |
92 |
return |
|
93 |
this.kind == Kind.STDOUT || |
|
94 |
this.kind == Kind.STDERR; |
|
95 |
} |
|
96 |
||
97 |
public boolean isSystem() { |
|
98 |
return |
|
99 |
this.kind == Kind.STDIN || |
|
100 |
this.kind == Kind.SIGNAL || |
|
101 |
this.kind == Kind.EXIT || |
|
25748 | 102 |
this.kind == Kind.PROMPT || |
25747 | 103 |
this.kind == Kind.SYSTEM; |
104 |
} |
|
105 |
||
25837
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
106 |
@Override |
25648 | 107 |
public String toString() { |
25807 | 108 |
if (this.props == null) { |
109 |
return this.kind.toString() + " [[" + this.result + "]]"; |
|
110 |
} else { |
|
111 |
return this.kind.toString() + " " + props.toString() + " [[" + this.result + "]]"; |
|
112 |
} |
|
25648 | 113 |
} |
114 |
} |
|
115 |
||
25745 | 116 |
|
117 |
/** |
|
118 |
* Main result queue -- accumulates cooked messages asynchronously. |
|
119 |
*/ |
|
25648 | 120 |
public LinkedBlockingQueue<Result> results; |
121 |
||
25807 | 122 |
private synchronized void putResult(Result.Kind kind, Properties props, String result) { |
25648 | 123 |
try { |
25807 | 124 |
results.put(new Result(kind, props, result)); |
25648 | 125 |
} catch (InterruptedException exn) { } |
126 |
} |
|
25807 | 127 |
private synchronized void putResult(Result.Kind kind, String result) { |
128 |
putResult(kind, null, result); |
|
129 |
} |
|
25648 | 130 |
|
131 |
||
25745 | 132 |
/** |
133 |
* Interrupts Isabelle process via Posix signal. |
|
134 |
* @throws isabelle.IsabelleProcess.IsabelleProcessException |
|
135 |
*/ |
|
25648 | 136 |
public synchronized void interrupt() throws IsabelleProcessException |
137 |
{ |
|
138 |
if (proc != null && pid != null) { |
|
25661 | 139 |
String kill = System.getProperty("isabelle.kill", "kill"); |
140 |
String [] cmdline = {kill, "-INT", pid}; |
|
25648 | 141 |
try { |
142 |
putResult(Result.Kind.SIGNAL, "INT"); |
|
25661 | 143 |
int rc = Runtime.getRuntime().exec(cmdline).waitFor(); |
25648 | 144 |
if (rc != 0) { |
145 |
throw new IsabelleProcessException("Cannot interrupt: kill command failed"); |
|
146 |
} |
|
147 |
} catch (IOException exn) { |
|
148 |
throw new IsabelleProcessException(exn.getMessage()); |
|
149 |
} catch (InterruptedException exn) { |
|
150 |
throw new IsabelleProcessException("Cannot interrupt: aborted"); |
|
151 |
} |
|
152 |
} else { |
|
153 |
throw new IsabelleProcessException("Cannot interrupt: no process"); |
|
154 |
} |
|
155 |
} |
|
156 |
||
157 |
||
25745 | 158 |
/** |
159 |
* Kills Isabelle process: try close -- sleep -- destroy. |
|
160 |
*/ |
|
25648 | 161 |
public synchronized void kill() throws IsabelleProcessException |
162 |
{ |
|
163 |
if (proc != null) { |
|
164 |
tryClose(); |
|
165 |
try { |
|
166 |
Thread.sleep(300); |
|
167 |
} catch (InterruptedException exn) { } |
|
168 |
putResult(Result.Kind.SIGNAL, "KILL"); |
|
169 |
proc.destroy(); |
|
170 |
proc = null; |
|
171 |
} else { |
|
172 |
throw new IsabelleProcessException("Cannot kill: no process"); |
|
173 |
} |
|
174 |
} |
|
175 |
||
25812 | 176 |
|
177 |
/** |
|
178 |
* Models basic Isabelle properties |
|
179 |
*/ |
|
180 |
public static class Property { |
|
181 |
public static String ID = "id"; |
|
182 |
public static String LINE = "line"; |
|
183 |
public static String FILE = "file"; |
|
184 |
} |
|
25648 | 185 |
|
25745 | 186 |
/** |
187 |
* Auxiliary operation to encode text as Isabelle string token. |
|
188 |
*/ |
|
25648 | 189 |
public static String encodeString(String str) { |
190 |
Locale locale = null; |
|
191 |
StringBuffer buf = new StringBuffer(100); |
|
192 |
int i; |
|
193 |
char c; |
|
194 |
||
195 |
buf.append("\""); |
|
196 |
for (i = 0; i < str.length(); i++) { |
|
197 |
c = str.charAt(i); |
|
198 |
if (c < 32 || c == '\\' || c == '\"') { |
|
199 |
buf.append(String.format(locale, "\\%03d", (int) c)); |
|
200 |
} else { |
|
201 |
buf.append(c); |
|
202 |
} |
|
203 |
} |
|
204 |
buf.append("\""); |
|
205 |
return buf.toString(); |
|
206 |
} |
|
207 |
||
25791 | 208 |
/** |
209 |
* Auxiliary operation to encode properties as Isabelle outer syntax. |
|
210 |
*/ |
|
211 |
public static String encodeProperties(Properties props) { |
|
212 |
StringBuffer buf = new StringBuffer(100); |
|
213 |
buf.append("("); |
|
214 |
for (Enumeration<String> e = (Enumeration<String>) props.propertyNames(); e.hasMoreElements(); ) { |
|
215 |
String x = e.nextElement(); |
|
216 |
buf.append(encodeString(x)); |
|
217 |
buf.append(" = "); |
|
218 |
buf.append(encodeString(props.getProperty(x))); |
|
219 |
if (e.hasMoreElements()) { |
|
220 |
buf.append(", "); |
|
221 |
} |
|
222 |
} |
|
223 |
buf.append(")"); |
|
224 |
return buf.toString(); |
|
225 |
} |
|
226 |
||
25648 | 227 |
|
228 |
/* output being piped into the process (stdin) */ |
|
229 |
||
230 |
private volatile BufferedWriter outputWriter; |
|
231 |
private class OutputThread extends Thread |
|
232 |
{ |
|
233 |
public void run() |
|
234 |
{ |
|
235 |
while (outputWriter != null) { |
|
236 |
try { |
|
237 |
String s = output.take(); |
|
238 |
if (s.equals("\u0000")) { |
|
239 |
outputWriter.close(); |
|
240 |
outputWriter = null; |
|
241 |
} else { |
|
242 |
putResult(Result.Kind.STDIN, s); |
|
243 |
outputWriter.write(s); |
|
244 |
outputWriter.flush(); |
|
245 |
} |
|
246 |
} catch (InterruptedException exn) { |
|
247 |
putResult(Result.Kind.SYSTEM, "Output thread interrupted"); |
|
248 |
} catch (IOException exn) { |
|
25791 | 249 |
putResult(Result.Kind.SYSTEM, exn.getMessage() + " (output thread)"); |
25648 | 250 |
} |
251 |
} |
|
252 |
putResult(Result.Kind.SYSTEM, "Output thread terminated"); |
|
253 |
} |
|
254 |
} |
|
255 |
private OutputThread outputThread; |
|
256 |
||
257 |
||
258 |
// public operations |
|
259 |
||
25745 | 260 |
/** |
261 |
* Feeds arbitrary text into the process. |
|
262 |
*/ |
|
25648 | 263 |
public synchronized void output(String text) throws IsabelleProcessException |
264 |
{ |
|
265 |
if (proc != null && !closing) { |
|
266 |
try { |
|
267 |
output.put(text); |
|
268 |
} catch (InterruptedException ex) { |
|
269 |
throw new IsabelleProcessException("Cannot output: aborted"); |
|
270 |
} |
|
271 |
} else if (proc == null) { |
|
272 |
throw new IsabelleProcessException("Cannot output: no process"); |
|
273 |
} else { |
|
274 |
throw new IsabelleProcessException("Cannot output: already closing"); |
|
275 |
} |
|
276 |
} |
|
277 |
||
25745 | 278 |
/** |
279 |
* Closes Isabelle process input, causing termination eventually. |
|
280 |
*/ |
|
25648 | 281 |
public synchronized void close() throws IsabelleProcessException |
282 |
{ |
|
283 |
output("\u0000"); |
|
284 |
closing = true; |
|
285 |
// FIXME watchdog/timeout |
|
286 |
} |
|
287 |
||
25745 | 288 |
/** |
289 |
* Closes Isabelle process input, causing termination eventually -- unless process already terminated. |
|
290 |
*/ |
|
25648 | 291 |
public synchronized void tryClose() |
292 |
{ |
|
293 |
if (proc != null && !closing) { |
|
294 |
try { |
|
295 |
close(); |
|
296 |
} catch (IsabelleProcessException ex) { } |
|
297 |
} |
|
298 |
} |
|
299 |
||
300 |
private synchronized void outputSync(String text) throws IsabelleProcessException |
|
301 |
{ |
|
302 |
output(" \\<^sync>\n; " + text + " \\<^sync>;\n"); |
|
303 |
} |
|
304 |
||
25745 | 305 |
/** |
25791 | 306 |
* Feeds exactly one Isabelle command into the process. |
25745 | 307 |
*/ |
25648 | 308 |
public synchronized void command(String text) throws IsabelleProcessException |
309 |
{ |
|
310 |
outputSync("Isabelle.command " + encodeString(text)); |
|
311 |
} |
|
312 |
||
25745 | 313 |
/** |
25791 | 314 |
* Isabelle command with properties. |
315 |
*/ |
|
316 |
public synchronized void command(Properties props, String text) throws IsabelleProcessException |
|
317 |
{ |
|
318 |
outputSync("Isabelle.command " + encodeProperties(props) + " " + encodeString(text)); |
|
319 |
} |
|
320 |
||
321 |
/** |
|
25745 | 322 |
* Feeds ML toplevel declarations into the process. |
323 |
*/ |
|
25648 | 324 |
public synchronized void ML(String text) throws IsabelleProcessException |
325 |
{ |
|
326 |
outputSync("ML " + encodeString(text)); |
|
327 |
} |
|
328 |
||
25791 | 329 |
/** |
330 |
* ML command with properties. |
|
331 |
*/ |
|
332 |
public synchronized void ML(Properties props, String text) throws IsabelleProcessException |
|
333 |
{ |
|
334 |
command(props, "ML " + encodeString(text)); |
|
335 |
} |
|
25648 | 336 |
|
25807 | 337 |
|
25648 | 338 |
/* input from the process (stdout/stderr) */ |
339 |
||
340 |
private volatile BufferedReader inputReader; |
|
341 |
private class InputThread extends Thread |
|
342 |
{ |
|
343 |
public void run() |
|
344 |
{ |
|
345 |
Result.Kind kind = Result.Kind.STDOUT; |
|
25807 | 346 |
Properties props = null; |
25648 | 347 |
StringBuffer buf = new StringBuffer(100); |
348 |
||
349 |
try { |
|
350 |
while (inputReader != null) { |
|
25837
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
351 |
if (kind == Result.Kind.STDOUT) { |
25648 | 352 |
// char mode |
353 |
int c = -1; |
|
354 |
while ((buf.length() == 0 || inputReader.ready()) && |
|
355 |
(c = inputReader.read()) > 0 && c != 2) { |
|
356 |
buf.append((char) c); |
|
357 |
} |
|
358 |
if (buf.length() > 0) { |
|
359 |
putResult(kind, buf.toString()); |
|
360 |
buf = new StringBuffer(100); |
|
361 |
} |
|
25807 | 362 |
if (c == -1) { |
363 |
inputReader.close(); |
|
364 |
inputReader = null; |
|
365 |
tryClose(); |
|
366 |
} |
|
367 |
else if (c == 2) { |
|
25648 | 368 |
c = inputReader.read(); |
369 |
switch (c) { |
|
370 |
case 'A': kind = Result.Kind.WRITELN; break; |
|
371 |
case 'B': kind = Result.Kind.PRIORITY; break; |
|
372 |
case 'C': kind = Result.Kind.TRACING; break; |
|
373 |
case 'D': kind = Result.Kind.WARNING; break; |
|
374 |
case 'E': kind = Result.Kind.ERROR; break; |
|
375 |
case 'F': kind = Result.Kind.DEBUG; break; |
|
25748 | 376 |
case 'G': kind = Result.Kind.PROMPT; break; |
25837
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
377 |
case 'H': kind = Result.Kind.INIT; break; |
25648 | 378 |
default: kind = Result.Kind.STDOUT; break; |
379 |
} |
|
25807 | 380 |
props = null; |
25648 | 381 |
} |
382 |
} else { |
|
383 |
// line mode |
|
384 |
String line = null; |
|
385 |
if ((line = inputReader.readLine()) != null) { |
|
25837
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
386 |
int len = line.length(); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
387 |
// property |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
388 |
if (line.endsWith("\u0002,")) { |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
389 |
int i = line.indexOf("="); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
390 |
if (i > 0) { |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
391 |
String name = line.substring(0, i); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
392 |
String value = line.substring(i + 1, len - 2); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
393 |
if (props == null) |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
394 |
props = new Properties(); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
395 |
if (!props.containsKey(name)) { |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
396 |
props.setProperty(name, value); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
397 |
} |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
398 |
} |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
399 |
} |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
400 |
// last text line |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
401 |
else if (line.endsWith("\u0002.")) { |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
402 |
if (kind == Result.Kind.INIT && props != null) { |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
403 |
pid = props.getProperty("pid"); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
404 |
session = props.getProperty("session"); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
405 |
} |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
406 |
buf.append(line.substring(0, len - 2)); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
407 |
putResult(kind, props, buf.toString()); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
408 |
buf = new StringBuffer(100); |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
409 |
kind = Result.Kind.STDOUT; |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
410 |
} |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
411 |
// text line |
2a7efcfe9b54
added INIT message, with pid and session property;
wenzelm
parents:
25812
diff
changeset
|
412 |
else { |
25648 | 413 |
buf.append(line); |
414 |
buf.append("\n"); |
|
415 |
} |
|
416 |
} else { |
|
417 |
inputReader.close(); |
|
418 |
inputReader = null; |
|
419 |
tryClose(); |
|
420 |
} |
|
421 |
} |
|
422 |
} |
|
423 |
} catch (IOException exn) { |
|
25791 | 424 |
putResult(Result.Kind.SYSTEM, exn.getMessage() + " (input thread)"); |
25648 | 425 |
} |
426 |
putResult(Result.Kind.SYSTEM, "Input thread terminated"); |
|
427 |
} |
|
428 |
} |
|
429 |
private InputThread inputThread; |
|
430 |
||
431 |
private volatile BufferedReader errorReader; |
|
432 |
private class ErrorThread extends Thread |
|
433 |
{ |
|
434 |
public void run() |
|
435 |
{ |
|
436 |
try { |
|
437 |
while (errorReader != null) { |
|
438 |
StringBuffer buf = new StringBuffer(100); |
|
439 |
int c; |
|
440 |
while ((buf.length() == 0 || errorReader.ready()) && (c = errorReader.read()) > 0) { |
|
441 |
buf.append((char) c); |
|
442 |
} |
|
443 |
if (buf.length() > 0) { |
|
444 |
putResult(Result.Kind.STDERR, buf.toString()); |
|
445 |
} else { |
|
446 |
errorReader.close(); |
|
447 |
errorReader = null; |
|
448 |
tryClose(); |
|
449 |
} |
|
450 |
} |
|
451 |
} catch (IOException exn) { |
|
25791 | 452 |
putResult(Result.Kind.SYSTEM, exn.getMessage() + " (error thread)"); |
25648 | 453 |
} |
454 |
putResult(Result.Kind.SYSTEM, "Error thread terminated"); |
|
455 |
} |
|
456 |
} |
|
457 |
private ErrorThread errorThread; |
|
458 |
||
459 |
||
460 |
/* exit thread */ |
|
461 |
||
462 |
private class ExitThread extends Thread |
|
463 |
{ |
|
464 |
public void run() |
|
465 |
{ |
|
466 |
try { |
|
467 |
int rc = proc.waitFor(); |
|
25649
9fc75df32c81
ExitThread: sleep(300) before delivering EXIT message;
wenzelm
parents:
25648
diff
changeset
|
468 |
Thread.sleep(300); |
25654 | 469 |
putResult(Result.Kind.SYSTEM, "Exit thread terminated"); |
25648 | 470 |
putResult(Result.Kind.EXIT, Integer.toString(rc)); |
471 |
proc = null; |
|
472 |
} catch (InterruptedException exn) { |
|
473 |
putResult(Result.Kind.SYSTEM, "Exit thread interrupted"); |
|
474 |
} |
|
475 |
} |
|
476 |
} |
|
477 |
private ExitThread exitThread; |
|
478 |
||
479 |
||
25745 | 480 |
/** |
481 |
* Creates Isabelle process with specified logic image. |
|
482 |
*/ |
|
25850 | 483 |
public IsabelleProcess(String [] options, String logic) throws IsabelleProcessException |
25648 | 484 |
{ |
25658
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
485 |
ArrayList<String> cmdline = new ArrayList<String> (); |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
486 |
String shell = null; |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
487 |
String home = null; |
25648 | 488 |
String charset = "UTF-8"; |
25659 | 489 |
|
25658
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
490 |
shell = System.getProperty("isabelle.shell"); |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
491 |
home = System.getProperty("isabelle.home"); |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
492 |
if (shell != null && home != null) { |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
493 |
cmdline.add(shell); |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
494 |
cmdline.add(home + "/bin/isabelle-process"); |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
495 |
} else if (home != null) { |
25659 | 496 |
cmdline.add(home + "/bin/isabelle-process"); |
25658
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
497 |
} else if (shell != null) { |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
498 |
throw new IsabelleProcessException("Cannot start process: isabelle.shell property requires isabelle.home"); |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
499 |
} else { |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
500 |
cmdline.add("isabelle-process"); |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
501 |
} |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
502 |
cmdline.add("-W"); |
25850 | 503 |
if (options != null) { |
504 |
for (String opt: options) cmdline.add(opt); |
|
505 |
} |
|
25661 | 506 |
if (logic != null) cmdline.add(logic); |
25658
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
507 |
|
25648 | 508 |
try { |
25658
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
509 |
String [] cmd = new String[cmdline.size()]; |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
510 |
cmdline.toArray(cmd); |
c3ae6c345fb5
compose command line according to isabelle.shell/home system properties;
wenzelm
parents:
25654
diff
changeset
|
511 |
proc = Runtime.getRuntime().exec(cmd); |
25648 | 512 |
} catch (IOException exn) { |
513 |
throw new IsabelleProcessException(exn.getMessage()); |
|
514 |
} |
|
515 |
||
516 |
try { |
|
517 |
outputWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream(), charset)); |
|
518 |
inputReader = new BufferedReader(new InputStreamReader(proc.getInputStream(), charset)); |
|
519 |
errorReader = new BufferedReader(new InputStreamReader(proc.getErrorStream(), charset)); |
|
520 |
} catch (UnsupportedEncodingException exn) { |
|
521 |
proc.destroy(); |
|
522 |
throw new Error(exn.getMessage()); |
|
523 |
} |
|
524 |
||
525 |
output = new LinkedBlockingQueue<String>(); |
|
526 |
outputThread = new OutputThread(); |
|
527 |
||
528 |
results = new LinkedBlockingQueue<Result>(); |
|
529 |
inputThread = new InputThread(); |
|
530 |
errorThread = new ErrorThread(); |
|
531 |
exitThread = new ExitThread(); |
|
532 |
||
533 |
outputThread.start(); |
|
534 |
inputThread.start(); |
|
535 |
errorThread.start(); |
|
536 |
exitThread.start(); |
|
537 |
} |
|
25791 | 538 |
|
25745 | 539 |
/** |
25850 | 540 |
* Creates Isabelle process without options. |
541 |
*/ |
|
542 |
public IsabelleProcess(String logic) throws IsabelleProcessException { |
|
543 |
this(null, logic); |
|
544 |
} |
|
545 |
||
546 |
/** |
|
25745 | 547 |
* Creates Isabelle process with default logic image. |
548 |
*/ |
|
25661 | 549 |
public IsabelleProcess() throws IsabelleProcessException { |
550 |
this(null); |
|
551 |
} |
|
25648 | 552 |
} |