12 public class IsabelleProcess { |
12 public class IsabelleProcess { |
13 private volatile Process proc; |
13 private volatile Process proc; |
14 private volatile String pid; |
14 private volatile String pid; |
15 private volatile boolean closing = false; |
15 private volatile boolean closing = false; |
16 private LinkedBlockingQueue<String> output; |
16 private LinkedBlockingQueue<String> output; |
|
17 |
17 |
18 |
18 /* exceptions */ |
19 /* exceptions */ |
19 |
20 |
20 public static class IsabelleProcessException extends Exception { |
21 public static class IsabelleProcessException extends Exception { |
21 public IsabelleProcessException() { |
22 public IsabelleProcessException() { |
25 super(msg); |
26 super(msg); |
26 } |
27 } |
27 }; |
28 }; |
28 |
29 |
29 |
30 |
30 /* main result queue */ |
31 /* results from the process */ |
31 |
32 |
32 public LinkedBlockingQueue<IsabelleResult> results; |
33 public static class Result { |
33 |
34 public enum Kind { |
34 private synchronized void putResult(IsabelleResult.Kind kind, String result) { |
35 STDOUT, STDERR, EXIT, // Posix results |
|
36 WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, // Isabelle results |
|
37 FAILURE // process wrapper problem |
|
38 }; |
|
39 public Kind kind; |
|
40 public String result; |
|
41 |
|
42 public Result(Kind kind, String result) { |
|
43 this.kind = kind; |
|
44 this.result = result; |
|
45 } |
|
46 |
|
47 public String toString() { |
|
48 return this.kind.toString() + " [[" + this.result + "]]"; |
|
49 } |
|
50 } |
|
51 |
|
52 public LinkedBlockingQueue<Result> results; |
|
53 |
|
54 private synchronized void putResult(Result.Kind kind, String result) { |
35 try { |
55 try { |
36 results.put(new IsabelleResult(kind, result)); |
56 results.put(new Result(kind, result)); |
37 } catch (InterruptedException exn) { } |
57 } catch (InterruptedException exn) { } |
38 } |
58 } |
39 |
59 |
40 |
60 |
41 /* encode arbitrary strings */ |
61 /* encode arbitrary strings */ |
101 String s = output.take(); |
121 String s = output.take(); |
102 if (s.equals("\u0000")) { |
122 if (s.equals("\u0000")) { |
103 outputWriter.close(); // FIXME timeout |
123 outputWriter.close(); // FIXME timeout |
104 outputWriter = null; |
124 outputWriter = null; |
105 } else { |
125 } else { |
106 System.err.println(s); |
|
107 outputWriter.write(s); |
126 outputWriter.write(s); |
108 outputWriter.flush(); |
127 outputWriter.flush(); |
109 } |
128 } |
110 } catch (InterruptedException exn) { |
129 } catch (InterruptedException exn) { |
111 putResult(IsabelleResult.Kind.FAILURE, "Cannot output: aborted"); |
130 putResult(Result.Kind.FAILURE, "Cannot output: aborted"); |
112 } catch (IOException exn) { |
131 } catch (IOException exn) { |
113 putResult(IsabelleResult.Kind.FAILURE, exn.getMessage()); |
132 putResult(Result.Kind.FAILURE, exn.getMessage()); |
114 } |
133 } |
115 } |
134 } |
116 } |
135 } |
117 } |
136 } |
118 private OutputThread outputThread; |
137 private OutputThread outputThread; |
169 |
188 |
170 private class InputThread extends Thread |
189 private class InputThread extends Thread |
171 { |
190 { |
172 public void run() |
191 public void run() |
173 { |
192 { |
174 IsabelleResult.Kind kind = IsabelleResult.Kind.STDOUT; |
193 Result.Kind kind = Result.Kind.STDOUT; |
175 StringBuffer buf = new StringBuffer(100); |
194 StringBuffer buf = new StringBuffer(100); |
176 |
195 |
177 try { |
196 try { |
178 while (inputReader != null) { |
197 while (inputReader != null) { |
179 if (kind == IsabelleResult.Kind.STDOUT && pid != null) { |
198 if (kind == Result.Kind.STDOUT && pid != null) { |
180 // char mode |
199 // char mode |
181 int c = 0; |
200 int c = 0; |
182 while ((buf.length() == 0 || inputReader.ready()) && |
201 while ((buf.length() == 0 || inputReader.ready()) && |
183 (c = inputReader.read()) > 0 && c != 2) { |
202 (c = inputReader.read()) > 0 && c != 2) { |
184 buf.append((char) c); |
203 buf.append((char) c); |
188 buf = new StringBuffer(100); |
207 buf = new StringBuffer(100); |
189 } |
208 } |
190 if (c == 2) { |
209 if (c == 2) { |
191 c = inputReader.read(); |
210 c = inputReader.read(); |
192 switch (c) { |
211 switch (c) { |
193 case 'A': kind = IsabelleResult.Kind.WRITELN; break; |
212 case 'A': kind = Result.Kind.WRITELN; break; |
194 case 'B': kind = IsabelleResult.Kind.PRIORITY; break; |
213 case 'B': kind = Result.Kind.PRIORITY; break; |
195 case 'C': kind = IsabelleResult.Kind.TRACING; break; |
214 case 'C': kind = Result.Kind.TRACING; break; |
196 case 'D': kind = IsabelleResult.Kind.WARNING; break; |
215 case 'D': kind = Result.Kind.WARNING; break; |
197 case 'E': kind = IsabelleResult.Kind.ERROR; break; |
216 case 'E': kind = Result.Kind.ERROR; break; |
198 case 'F': kind = IsabelleResult.Kind.DEBUG; break; |
217 case 'F': kind = Result.Kind.DEBUG; break; |
199 default: kind = IsabelleResult.Kind.STDOUT; break; |
218 default: kind = Result.Kind.STDOUT; break; |
200 } |
219 } |
201 } |
220 } |
202 } else { |
221 } else { |
203 // line mode |
222 // line mode |
204 String line = null; |
223 String line = null; |
205 if ((line = inputReader.readLine()) != null) { |
224 if ((line = inputReader.readLine()) != null) { |
206 if (pid == null && kind == IsabelleResult.Kind.STDOUT && line.startsWith("PID=")) { |
225 if (pid == null && kind == Result.Kind.STDOUT && line.startsWith("PID=")) { |
207 pid = line.substring("PID=".length()); |
226 pid = line.substring("PID=".length()); |
208 } else if (kind == IsabelleResult.Kind.STDOUT) { |
227 } else if (kind == Result.Kind.STDOUT) { |
209 buf.append(line); |
228 buf.append(line); |
210 buf.append("\n"); |
229 buf.append("\n"); |
211 putResult(kind, buf.toString()); |
230 putResult(kind, buf.toString()); |
212 buf = new StringBuffer(100); |
231 buf = new StringBuffer(100); |
213 } else { |
232 } else { |
214 int len = line.length(); |
233 int len = line.length(); |
215 if (len >= 2 && line.charAt(len - 2) == 2 && line.charAt(len - 1) == '.') { |
234 if (len >= 2 && line.charAt(len - 2) == 2 && line.charAt(len - 1) == '.') { |
216 buf.append(line.substring(0, len - 2)); |
235 buf.append(line.substring(0, len - 2)); |
217 putResult(kind, buf.toString()); |
236 putResult(kind, buf.toString()); |
218 buf = new StringBuffer(100); |
237 buf = new StringBuffer(100); |
219 kind = IsabelleResult.Kind.STDOUT; |
238 kind = Result.Kind.STDOUT; |
220 } else { |
239 } else { |
221 buf.append(line); |
240 buf.append(line); |
222 buf.append("\n"); |
241 buf.append("\n"); |
223 } |
242 } |
224 } |
243 } |
247 int c; |
266 int c; |
248 while ((buf.length() == 0 || errorReader.ready()) && (c = errorReader.read()) > 0) { |
267 while ((buf.length() == 0 || errorReader.ready()) && (c = errorReader.read()) > 0) { |
249 buf.append((char) c); |
268 buf.append((char) c); |
250 } |
269 } |
251 if (buf.length() > 0) { |
270 if (buf.length() > 0) { |
252 putResult(IsabelleResult.Kind.STDERR, buf.toString()); |
271 putResult(Result.Kind.STDERR, buf.toString()); |
253 } else { |
272 } else { |
254 errorReader.close(); |
273 errorReader.close(); |
255 errorReader = null; |
274 errorReader = null; |
256 checkTermination(); |
275 checkTermination(); |
257 } |
276 } |
258 } |
277 } |
259 } catch (IOException exn) { |
278 } catch (IOException exn) { |
260 putResult(IsabelleResult.Kind.FAILURE, exn.getMessage()); |
279 putResult(Result.Kind.FAILURE, exn.getMessage()); |
261 } |
280 } |
262 System.err.println("Error thread terminated"); |
281 System.err.println("Error thread terminated"); |
263 } |
282 } |
264 } |
283 } |
265 private ErrorThread errorThread; |
284 private ErrorThread errorThread; |
269 |
288 |
270 private class ConsoleThread extends Thread |
289 private class ConsoleThread extends Thread |
271 { |
290 { |
272 public void run() |
291 public void run() |
273 { |
292 { |
274 IsabelleResult result = null; |
293 Result result = null; |
275 while (result == null || result.kind != IsabelleResult.Kind.EXIT) { |
294 while (result == null || result.kind != Result.Kind.EXIT) { |
276 try { |
295 try { |
277 result = results.take(); |
296 result = results.take(); |
278 System.err.println(result.toString()); |
297 System.err.println(result.toString()); |
279 } catch (InterruptedException ex) { |
298 } catch (InterruptedException ex) { |
280 putResult(IsabelleResult.Kind.FAILURE, "Cannot interrupt: aborted"); |
299 putResult(Result.Kind.FAILURE, "Cannot interrupt: aborted"); |
281 } |
300 } |
282 } |
301 } |
283 System.err.println("Console thread terminated"); |
302 System.err.println("Console thread terminated"); |
284 } |
303 } |
285 } |
304 } |
298 |
317 |
299 output = new LinkedBlockingQueue<String>(); |
318 output = new LinkedBlockingQueue<String>(); |
300 outputWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream(), charset)); |
319 outputWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream(), charset)); |
301 outputThread = new OutputThread(); |
320 outputThread = new OutputThread(); |
302 |
321 |
303 results = new LinkedBlockingQueue<IsabelleResult>(); |
322 results = new LinkedBlockingQueue<Result>(); |
304 inputReader = new BufferedReader(new InputStreamReader(proc.getInputStream(), charset)); |
323 inputReader = new BufferedReader(new InputStreamReader(proc.getInputStream(), charset)); |
305 errorReader = new BufferedReader(new InputStreamReader(proc.getErrorStream(), charset)); |
324 errorReader = new BufferedReader(new InputStreamReader(proc.getErrorStream(), charset)); |
306 inputThread = new InputThread(); |
325 inputThread = new InputThread(); |
307 errorThread = new ErrorThread(); |
326 errorThread = new ErrorThread(); |
308 |
327 |