|
1 /* |
|
2 * IsabelleProcess.java |
|
3 * |
|
4 * $Id$ |
|
5 * |
|
6 */ |
|
7 |
|
8 import java.io.*; |
|
9 import java.util.Locale; |
|
10 import java.util.concurrent.LinkedBlockingQueue; |
|
11 |
|
12 public class IsabelleProcess { |
|
13 private volatile Process proc; |
|
14 private volatile String pid; |
|
15 private volatile boolean closing = false; |
|
16 private LinkedBlockingQueue<String> output; |
|
17 |
|
18 /* exceptions */ |
|
19 |
|
20 public static class IsabelleProcessException extends Exception { |
|
21 public IsabelleProcessException() { |
|
22 super(); |
|
23 } |
|
24 public IsabelleProcessException(String msg) { |
|
25 super(msg); |
|
26 } |
|
27 }; |
|
28 |
|
29 |
|
30 /* main result queue */ |
|
31 |
|
32 public LinkedBlockingQueue<IsabelleResult> results; |
|
33 |
|
34 private synchronized void putResult(IsabelleResult.Kind kind, String result) { |
|
35 try { |
|
36 results.put(new IsabelleResult(kind, result)); |
|
37 } catch (InterruptedException exn) { } |
|
38 } |
|
39 |
|
40 |
|
41 /* encode arbitrary strings */ |
|
42 |
|
43 public static String encodeString(String str) { |
|
44 Locale locale = null; |
|
45 StringBuffer buf = new StringBuffer(100); |
|
46 int i; |
|
47 char c; |
|
48 |
|
49 buf.append("\""); |
|
50 for (i = 0; i < str.length(); i++) { |
|
51 c = str.charAt(i); |
|
52 if (c < 32 || c == '\\' || c == '\"') { |
|
53 buf.append(String.format(locale, "\\%03d", (int) c)); |
|
54 } else { |
|
55 buf.append(c); |
|
56 } |
|
57 } |
|
58 buf.append("\""); |
|
59 return buf.toString(); |
|
60 } |
|
61 |
|
62 |
|
63 /* interrupt process */ |
|
64 |
|
65 public synchronized void interrupt() throws IsabelleProcessException |
|
66 { |
|
67 if (proc != null && pid != null) { |
|
68 try { |
|
69 int rc = Runtime.getRuntime().exec("kill -INT " + pid).waitFor(); |
|
70 if (rc != 0) { |
|
71 throw new IsabelleProcessException("Cannot interrupt: kill failed"); |
|
72 } |
|
73 } catch (IOException exn) { |
|
74 throw new IsabelleProcessException(exn.getMessage()); |
|
75 } catch (InterruptedException exn) { |
|
76 throw new IsabelleProcessException("Cannot interrupt: aborted"); |
|
77 } |
|
78 } else { |
|
79 throw new IsabelleProcessException("Cannot interrupt: no process"); |
|
80 } |
|
81 } |
|
82 |
|
83 |
|
84 /* terminate process */ |
|
85 |
|
86 public synchronized void terminate() |
|
87 { |
|
88 // FIXME |
|
89 } |
|
90 |
|
91 |
|
92 /* output being piped into the process (stdin) */ |
|
93 |
|
94 private volatile BufferedWriter outputWriter; |
|
95 private class OutputThread extends Thread |
|
96 { |
|
97 public void run() |
|
98 { |
|
99 while (outputWriter != null) { |
|
100 try { |
|
101 String s = output.take(); |
|
102 if (s.equals("\u0000")) { |
|
103 outputWriter.close(); // FIXME timeout |
|
104 outputWriter = null; |
|
105 } else { |
|
106 System.err.println(s); |
|
107 outputWriter.write(s); |
|
108 outputWriter.flush(); |
|
109 } |
|
110 } catch (InterruptedException exn) { |
|
111 putResult(IsabelleResult.Kind.FAILURE, "Cannot output: aborted"); |
|
112 } catch (IOException exn) { |
|
113 putResult(IsabelleResult.Kind.FAILURE, exn.getMessage()); |
|
114 } |
|
115 } |
|
116 } |
|
117 } |
|
118 private OutputThread outputThread; |
|
119 |
|
120 |
|
121 // public operations |
|
122 |
|
123 public synchronized void output(String text) throws IsabelleProcessException |
|
124 { |
|
125 if (!closing) { |
|
126 try { |
|
127 output.put(text); |
|
128 } catch (InterruptedException ex) { |
|
129 throw new IsabelleProcessException("Cannot output: aborted"); |
|
130 } |
|
131 } else { |
|
132 throw new IsabelleProcessException("Cannot output: already closing"); |
|
133 } |
|
134 } |
|
135 |
|
136 private synchronized void commandWrapping(String cmd, String text) throws IsabelleProcessException |
|
137 { |
|
138 output(" \\<^sync> " + cmd + " " + encodeString(text) + " \\<^sync>;\n"); |
|
139 } |
|
140 |
|
141 public synchronized void command(String text) throws IsabelleProcessException |
|
142 { |
|
143 commandWrapping("Isabelle.command", text); |
|
144 } |
|
145 |
|
146 public synchronized void ML(String text) throws IsabelleProcessException |
|
147 { |
|
148 commandWrapping("ML", text); |
|
149 } |
|
150 |
|
151 public synchronized void close() throws IsabelleProcessException |
|
152 { |
|
153 output("\u0000"); |
|
154 closing = true; |
|
155 } |
|
156 |
|
157 |
|
158 /* input being read from the process (stdout/stderr) */ |
|
159 |
|
160 private volatile BufferedReader inputReader; |
|
161 private volatile BufferedReader errorReader; |
|
162 |
|
163 private synchronized void checkTermination() |
|
164 { |
|
165 if (inputReader == null && errorReader == null) { |
|
166 terminate(); |
|
167 } |
|
168 } |
|
169 |
|
170 private class InputThread extends Thread |
|
171 { |
|
172 public void run() |
|
173 { |
|
174 IsabelleResult.Kind kind = IsabelleResult.Kind.STDOUT; |
|
175 StringBuffer buf = new StringBuffer(100); |
|
176 |
|
177 try { |
|
178 while (inputReader != null) { |
|
179 if (kind == IsabelleResult.Kind.STDOUT && pid != null) { |
|
180 // char mode |
|
181 int c = 0; |
|
182 while ((buf.length() == 0 || inputReader.ready()) && |
|
183 (c = inputReader.read()) > 0 && c != 2) { |
|
184 buf.append((char) c); |
|
185 } |
|
186 if (buf.length() > 0) { |
|
187 putResult(kind, buf.toString()); |
|
188 buf = new StringBuffer(100); |
|
189 } |
|
190 if (c == 2) { |
|
191 c = inputReader.read(); |
|
192 switch (c) { |
|
193 case 'A': kind = IsabelleResult.Kind.WRITELN; break; |
|
194 case 'B': kind = IsabelleResult.Kind.PRIORITY; break; |
|
195 case 'C': kind = IsabelleResult.Kind.TRACING; break; |
|
196 case 'D': kind = IsabelleResult.Kind.WARNING; break; |
|
197 case 'E': kind = IsabelleResult.Kind.ERROR; break; |
|
198 case 'F': kind = IsabelleResult.Kind.DEBUG; break; |
|
199 default: kind = IsabelleResult.Kind.STDOUT; break; |
|
200 } |
|
201 } |
|
202 } else { |
|
203 // line mode |
|
204 String line = null; |
|
205 if ((line = inputReader.readLine()) != null) { |
|
206 if (pid == null && kind == IsabelleResult.Kind.STDOUT && line.startsWith("PID=")) { |
|
207 pid = line.substring("PID=".length()); |
|
208 } else if (kind == IsabelleResult.Kind.STDOUT) { |
|
209 buf.append(line); |
|
210 buf.append("\n"); |
|
211 putResult(kind, buf.toString()); |
|
212 buf = new StringBuffer(100); |
|
213 } else { |
|
214 int len = line.length(); |
|
215 if (len >= 2 && line.charAt(len - 2) == 2 && line.charAt(len - 1) == '.') { |
|
216 buf.append(line.substring(0, len - 2)); |
|
217 putResult(kind, buf.toString()); |
|
218 buf = new StringBuffer(100); |
|
219 kind = IsabelleResult.Kind.STDOUT; |
|
220 } else { |
|
221 buf.append(line); |
|
222 buf.append("\n"); |
|
223 } |
|
224 } |
|
225 } else { |
|
226 inputReader.close(); |
|
227 inputReader = null; |
|
228 checkTermination(); |
|
229 } |
|
230 } |
|
231 } |
|
232 } catch (IOException exn) { |
|
233 putResult(IsabelleResult.Kind.FAILURE, exn.getMessage()); |
|
234 } |
|
235 System.err.println("Input thread terminated"); |
|
236 } |
|
237 } |
|
238 private InputThread inputThread; |
|
239 |
|
240 private class ErrorThread extends Thread |
|
241 { |
|
242 public void run() |
|
243 { |
|
244 try { |
|
245 while (errorReader != null) { |
|
246 StringBuffer buf = new StringBuffer(100); |
|
247 int c; |
|
248 while ((buf.length() == 0 || errorReader.ready()) && (c = errorReader.read()) > 0) { |
|
249 buf.append((char) c); |
|
250 } |
|
251 if (buf.length() > 0) { |
|
252 putResult(IsabelleResult.Kind.STDERR, buf.toString()); |
|
253 } else { |
|
254 errorReader.close(); |
|
255 errorReader = null; |
|
256 checkTermination(); |
|
257 } |
|
258 } |
|
259 } catch (IOException exn) { |
|
260 putResult(IsabelleResult.Kind.FAILURE, exn.getMessage()); |
|
261 } |
|
262 System.err.println("Error thread terminated"); |
|
263 } |
|
264 } |
|
265 private ErrorThread errorThread; |
|
266 |
|
267 |
|
268 /* console thread -- demo */ |
|
269 |
|
270 private class ConsoleThread extends Thread |
|
271 { |
|
272 public void run() |
|
273 { |
|
274 IsabelleResult result = null; |
|
275 while (result == null || result.kind != IsabelleResult.Kind.EXIT) { |
|
276 try { |
|
277 result = results.take(); |
|
278 System.err.println(result.toString()); |
|
279 } catch (InterruptedException ex) { |
|
280 putResult(IsabelleResult.Kind.FAILURE, "Cannot interrupt: aborted"); |
|
281 } |
|
282 } |
|
283 System.err.println("Console thread terminated"); |
|
284 } |
|
285 } |
|
286 private ConsoleThread consoleThread; |
|
287 |
|
288 |
|
289 /* create process */ |
|
290 |
|
291 public IsabelleProcess(String logic) throws IsabelleProcessException |
|
292 { |
|
293 String [] cmdline = {"isabelle", "-W", logic}; |
|
294 String charset = "UTF-8"; |
|
295 try { |
|
296 proc = Runtime.getRuntime().exec(cmdline); |
|
297 pid = null; |
|
298 |
|
299 output = new LinkedBlockingQueue<String>(); |
|
300 outputWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream(), charset)); |
|
301 outputThread = new OutputThread(); |
|
302 |
|
303 results = new LinkedBlockingQueue<IsabelleResult>(); |
|
304 inputReader = new BufferedReader(new InputStreamReader(proc.getInputStream(), charset)); |
|
305 errorReader = new BufferedReader(new InputStreamReader(proc.getErrorStream(), charset)); |
|
306 inputThread = new InputThread(); |
|
307 errorThread = new ErrorThread(); |
|
308 |
|
309 consoleThread = new ConsoleThread(); |
|
310 } catch (IOException exn) { |
|
311 terminate(); |
|
312 throw new IsabelleProcessException(exn.getMessage()); |
|
313 } |
|
314 |
|
315 outputThread.start(); |
|
316 inputThread.start(); |
|
317 errorThread.start(); |
|
318 consoleThread.start(); |
|
319 } |
|
320 } |