wenzelm@27963
|
1 |
/* Title: Pure/Tools/isabelle_process.ML
|
wenzelm@27949
|
2 |
ID: $Id$
|
wenzelm@27949
|
3 |
Author: Makarius
|
wenzelm@27963
|
4 |
Options: :folding=explicit:collapseFolds=1:
|
wenzelm@27949
|
5 |
|
wenzelm@27949
|
6 |
Isabelle process management -- always reactive due to multi-threaded I/O.
|
wenzelm@27949
|
7 |
*/
|
wenzelm@27949
|
8 |
|
wenzelm@27949
|
9 |
package isabelle
|
wenzelm@27949
|
10 |
|
wenzelm@27949
|
11 |
import java.util.Properties
|
wenzelm@27955
|
12 |
import java.util.concurrent.LinkedBlockingQueue
|
wenzelm@27949
|
13 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, IOException}
|
wenzelm@27949
|
14 |
|
wenzelm@27963
|
15 |
import isabelle.{Symbol, XML}
|
wenzelm@27949
|
16 |
|
wenzelm@27949
|
17 |
|
wenzelm@27973
|
18 |
object IsabelleProcess {
|
wenzelm@27973
|
19 |
|
wenzelm@27949
|
20 |
/* results */
|
wenzelm@27949
|
21 |
|
wenzelm@27949
|
22 |
object Kind extends Enumeration {
|
wenzelm@27949
|
23 |
//{{{ values
|
wenzelm@27949
|
24 |
// Posix channels/events
|
wenzelm@27949
|
25 |
val STDIN = Value("STDIN")
|
wenzelm@27949
|
26 |
val STDOUT = Value("STDOUT")
|
wenzelm@27949
|
27 |
val STDERR = Value("STDERR")
|
wenzelm@27949
|
28 |
val SIGNAL = Value("SIGNAL")
|
wenzelm@27949
|
29 |
val EXIT = Value("EXIT")
|
wenzelm@27949
|
30 |
// Isabelle messages
|
wenzelm@27949
|
31 |
val WRITELN = Value("WRITELN")
|
wenzelm@27949
|
32 |
val PRIORITY = Value("PRIORITY")
|
wenzelm@27949
|
33 |
val TRACING = Value("TRACING")
|
wenzelm@27949
|
34 |
val WARNING = Value("WARNING")
|
wenzelm@27949
|
35 |
val ERROR = Value("ERROR")
|
wenzelm@27949
|
36 |
val DEBUG = Value("DEBUG")
|
wenzelm@27949
|
37 |
val PROMPT = Value("PROMPT")
|
wenzelm@27949
|
38 |
val INIT = Value("INIT")
|
wenzelm@27949
|
39 |
val STATUS = Value("STATUS")
|
wenzelm@27949
|
40 |
// internal system notification
|
wenzelm@27949
|
41 |
val SYSTEM = Value("SYSTEM")
|
wenzelm@27949
|
42 |
//}}}
|
wenzelm@27949
|
43 |
def is_raw(kind: Value) =
|
wenzelm@27949
|
44 |
kind == STDOUT ||
|
wenzelm@27949
|
45 |
kind == STDERR
|
wenzelm@27990
|
46 |
def is_control(kind: Value) =
|
wenzelm@27990
|
47 |
kind == SIGNAL ||
|
wenzelm@27990
|
48 |
kind == EXIT ||
|
wenzelm@27990
|
49 |
kind == SYSTEM
|
wenzelm@27949
|
50 |
def is_system(kind: Value) =
|
wenzelm@27949
|
51 |
kind == STDIN ||
|
wenzelm@27949
|
52 |
kind == SIGNAL ||
|
wenzelm@27949
|
53 |
kind == EXIT ||
|
wenzelm@27949
|
54 |
kind == PROMPT ||
|
wenzelm@27949
|
55 |
kind == STATUS ||
|
wenzelm@27949
|
56 |
kind == SYSTEM
|
wenzelm@27949
|
57 |
}
|
wenzelm@27949
|
58 |
|
wenzelm@27973
|
59 |
class Result(val kind: Kind.Value, val props: Properties, val result: String) {
|
wenzelm@27949
|
60 |
override def toString = {
|
wenzelm@27963
|
61 |
val res = XML.content(YXML.parse_failsafe(result)).mkString("")
|
wenzelm@27955
|
62 |
if (props == null) kind.toString + " [[" + res + "]]"
|
wenzelm@27955
|
63 |
else kind.toString + " " + props.toString + " [[" + res + "]]"
|
wenzelm@27949
|
64 |
}
|
wenzelm@27973
|
65 |
def is_raw() = Kind.is_raw(kind)
|
wenzelm@27990
|
66 |
def is_control() = Kind.is_control(kind)
|
wenzelm@27973
|
67 |
def is_system() = Kind.is_system(kind)
|
wenzelm@27973
|
68 |
}
|
wenzelm@27949
|
69 |
|
wenzelm@27973
|
70 |
}
|
wenzelm@27973
|
71 |
|
wenzelm@27973
|
72 |
|
wenzelm@27973
|
73 |
class IsabelleProcess(args: String*) {
|
wenzelm@27973
|
74 |
|
wenzelm@27973
|
75 |
import IsabelleProcess._
|
wenzelm@27973
|
76 |
|
wenzelm@27973
|
77 |
|
wenzelm@27973
|
78 |
/* process information */
|
wenzelm@27973
|
79 |
|
wenzelm@27973
|
80 |
private var proc: Process = null
|
wenzelm@27973
|
81 |
private var closing = false
|
wenzelm@27973
|
82 |
private var pid: String = null
|
wenzelm@27973
|
83 |
private var the_session: String = null
|
wenzelm@27973
|
84 |
def session() = the_session
|
wenzelm@27973
|
85 |
|
wenzelm@27973
|
86 |
|
wenzelm@27990
|
87 |
/* symbols */
|
wenzelm@27990
|
88 |
|
wenzelm@27990
|
89 |
val symbols = new Symbol.Interpretation
|
wenzelm@27990
|
90 |
def decode_result(result: Result) = YXML.parse_failsafe(symbols.decode(result.result))
|
wenzelm@27990
|
91 |
|
wenzelm@27990
|
92 |
|
wenzelm@27973
|
93 |
/* results */
|
wenzelm@27949
|
94 |
|
wenzelm@27990
|
95 |
private val results = new LinkedBlockingQueue[Result]
|
wenzelm@27949
|
96 |
|
wenzelm@27949
|
97 |
private def put_result(kind: Kind.Value, props: Properties, result: String) {
|
wenzelm@27963
|
98 |
if (kind == Kind.INIT && props != null) {
|
wenzelm@27973
|
99 |
pid = props.getProperty(Markup.PID)
|
wenzelm@27973
|
100 |
the_session = props.getProperty(Markup.SESSION)
|
wenzelm@27963
|
101 |
}
|
wenzelm@27955
|
102 |
results.put(new Result(kind, props, result))
|
wenzelm@27949
|
103 |
}
|
wenzelm@27949
|
104 |
|
wenzelm@27990
|
105 |
def get_result() = results.take
|
wenzelm@27973
|
106 |
|
wenzelm@27992
|
107 |
def try_result() = {
|
wenzelm@27992
|
108 |
val res = results.poll
|
wenzelm@27992
|
109 |
if (res != null) Some(res) else None
|
wenzelm@27992
|
110 |
}
|
wenzelm@27992
|
111 |
|
wenzelm@27973
|
112 |
|
wenzelm@27973
|
113 |
/* signals */
|
wenzelm@27973
|
114 |
|
wenzelm@27973
|
115 |
def interrupt() = synchronized {
|
wenzelm@27993
|
116 |
if (proc == null) error("Cannot interrupt Isabelle: no process")
|
wenzelm@27973
|
117 |
if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
|
wenzelm@27973
|
118 |
else {
|
wenzelm@27973
|
119 |
try {
|
wenzelm@27990
|
120 |
if (IsabelleSystem.exec(List("kill", "-INT", pid)).waitFor == 0)
|
wenzelm@27990
|
121 |
put_result(Kind.SIGNAL, null, "INT")
|
wenzelm@27990
|
122 |
else
|
wenzelm@27973
|
123 |
put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
|
wenzelm@27973
|
124 |
}
|
wenzelm@27993
|
125 |
catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
|
wenzelm@27973
|
126 |
}
|
wenzelm@27973
|
127 |
}
|
wenzelm@27973
|
128 |
|
wenzelm@27973
|
129 |
def kill() = synchronized {
|
wenzelm@27993
|
130 |
if (proc == 0) error("Cannot kill Isabelle: no process")
|
wenzelm@27973
|
131 |
else {
|
wenzelm@27973
|
132 |
try_close()
|
wenzelm@27990
|
133 |
Thread.sleep(500)
|
wenzelm@27973
|
134 |
put_result(Kind.SIGNAL, null, "KILL")
|
wenzelm@27973
|
135 |
proc.destroy
|
wenzelm@27973
|
136 |
proc = null
|
wenzelm@27990
|
137 |
pid = null
|
wenzelm@27973
|
138 |
}
|
wenzelm@27973
|
139 |
}
|
wenzelm@27973
|
140 |
|
wenzelm@27949
|
141 |
|
wenzelm@27949
|
142 |
/* output being piped into the process */
|
wenzelm@27949
|
143 |
|
wenzelm@27990
|
144 |
private val output = new LinkedBlockingQueue[String]
|
wenzelm@27949
|
145 |
|
wenzelm@27949
|
146 |
def output_raw(text: String) = synchronized {
|
wenzelm@27993
|
147 |
if (proc == null) error("Cannot output to Isabelle: no process")
|
wenzelm@27993
|
148 |
if (closing) error("Cannot output to Isabelle: already closing")
|
wenzelm@27955
|
149 |
output.put(text)
|
wenzelm@27949
|
150 |
}
|
wenzelm@27949
|
151 |
|
wenzelm@27949
|
152 |
def output_sync(text: String) = output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
|
wenzelm@27949
|
153 |
|
wenzelm@27963
|
154 |
|
wenzelm@27963
|
155 |
def command(text: String) =
|
wenzelm@27949
|
156 |
output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
|
wenzelm@27949
|
157 |
|
wenzelm@27963
|
158 |
def command(props: Properties, text: String) =
|
wenzelm@27949
|
159 |
output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
|
wenzelm@27949
|
160 |
IsabelleSyntax.encode_string(text))
|
wenzelm@27949
|
161 |
|
wenzelm@27963
|
162 |
def ML(text: String) =
|
wenzelm@27949
|
163 |
output_sync("ML_val " + IsabelleSyntax.encode_string(text))
|
wenzelm@27949
|
164 |
|
wenzelm@27949
|
165 |
def close() = synchronized { // FIXME watchdog/timeout
|
wenzelm@27949
|
166 |
output_raw("\u0000")
|
wenzelm@27949
|
167 |
closing = true
|
wenzelm@27949
|
168 |
}
|
wenzelm@27949
|
169 |
|
wenzelm@27949
|
170 |
def try_close() = synchronized {
|
wenzelm@27949
|
171 |
if (proc != null && !closing) {
|
wenzelm@27949
|
172 |
try { close() }
|
wenzelm@27993
|
173 |
catch { case _: RuntimeException => }
|
wenzelm@27949
|
174 |
}
|
wenzelm@27949
|
175 |
}
|
wenzelm@27949
|
176 |
|
wenzelm@27949
|
177 |
|
wenzelm@27949
|
178 |
/* stdin */
|
wenzelm@27949
|
179 |
|
wenzelm@27949
|
180 |
private class StdinThread(writer: BufferedWriter) extends Thread {
|
wenzelm@27949
|
181 |
override def run() = {
|
wenzelm@27949
|
182 |
var finished = false
|
wenzelm@27949
|
183 |
while (!finished) {
|
wenzelm@27949
|
184 |
try {
|
wenzelm@27949
|
185 |
//{{{
|
wenzelm@27955
|
186 |
val s = output.take
|
wenzelm@27949
|
187 |
if (s == "\u0000") {
|
wenzelm@27949
|
188 |
writer.close
|
wenzelm@27949
|
189 |
finished = true
|
wenzelm@27949
|
190 |
}
|
wenzelm@27949
|
191 |
else {
|
wenzelm@27949
|
192 |
put_result(Kind.STDIN, null, s)
|
wenzelm@27949
|
193 |
writer.write(s)
|
wenzelm@27949
|
194 |
writer.flush
|
wenzelm@27949
|
195 |
}
|
wenzelm@27949
|
196 |
//}}}
|
wenzelm@27949
|
197 |
}
|
wenzelm@27949
|
198 |
catch {
|
wenzelm@27949
|
199 |
case e: IOException => put_result(Kind.SYSTEM, null, "Stdin thread: " + e.getMessage)
|
wenzelm@27949
|
200 |
}
|
wenzelm@27949
|
201 |
}
|
wenzelm@27949
|
202 |
put_result(Kind.SYSTEM, null, "Stdin thread terminated")
|
wenzelm@27949
|
203 |
}
|
wenzelm@27949
|
204 |
}
|
wenzelm@27949
|
205 |
|
wenzelm@27949
|
206 |
|
wenzelm@27949
|
207 |
/* stdout */
|
wenzelm@27949
|
208 |
|
wenzelm@27949
|
209 |
private class StdoutThread(reader: BufferedReader) extends Thread {
|
wenzelm@27949
|
210 |
override def run() = {
|
wenzelm@27949
|
211 |
var kind = Kind.STDOUT
|
wenzelm@27949
|
212 |
var props: Properties = null
|
wenzelm@27949
|
213 |
var result = new StringBuilder
|
wenzelm@27949
|
214 |
|
wenzelm@27949
|
215 |
var finished = false
|
wenzelm@27949
|
216 |
while (!finished) {
|
wenzelm@27949
|
217 |
try {
|
wenzelm@27949
|
218 |
if (kind == Kind.STDOUT) {
|
wenzelm@27949
|
219 |
//{{{ Char mode
|
wenzelm@27949
|
220 |
var c = -1
|
wenzelm@27949
|
221 |
var done = false
|
wenzelm@27949
|
222 |
while (!done && (result.length == 0 || reader.ready)) {
|
wenzelm@27949
|
223 |
c = reader.read
|
wenzelm@27949
|
224 |
if (c > 0 && c != 2) result.append(c.asInstanceOf[Char])
|
wenzelm@27949
|
225 |
else done = true
|
wenzelm@27949
|
226 |
}
|
wenzelm@27949
|
227 |
if (result.length > 0) {
|
wenzelm@27949
|
228 |
put_result(kind, null, result.toString)
|
wenzelm@27949
|
229 |
result.length = 0
|
wenzelm@27949
|
230 |
}
|
wenzelm@27949
|
231 |
if (c == -1) {
|
wenzelm@27949
|
232 |
reader.close
|
wenzelm@27949
|
233 |
finished = true
|
wenzelm@27949
|
234 |
try_close()
|
wenzelm@27949
|
235 |
}
|
wenzelm@27949
|
236 |
else if (c == 2) {
|
wenzelm@27949
|
237 |
reader.read match {
|
wenzelm@27949
|
238 |
case 'A' => kind = Kind.WRITELN
|
wenzelm@27949
|
239 |
case 'B' => kind = Kind.PRIORITY
|
wenzelm@27949
|
240 |
case 'C' => kind = Kind.TRACING
|
wenzelm@27949
|
241 |
case 'D' => kind = Kind.WARNING
|
wenzelm@27949
|
242 |
case 'E' => kind = Kind.ERROR
|
wenzelm@27949
|
243 |
case 'F' => kind = Kind.DEBUG
|
wenzelm@27949
|
244 |
case 'G' => kind = Kind.PROMPT
|
wenzelm@27949
|
245 |
case 'H' => kind = Kind.INIT
|
wenzelm@27949
|
246 |
case 'I' => kind = Kind.STATUS
|
wenzelm@27949
|
247 |
case _ => kind = Kind.STDOUT
|
wenzelm@27949
|
248 |
}
|
wenzelm@27949
|
249 |
props = null
|
wenzelm@27949
|
250 |
}
|
wenzelm@27949
|
251 |
//}}}
|
wenzelm@27949
|
252 |
}
|
wenzelm@27949
|
253 |
else {
|
wenzelm@27949
|
254 |
//{{{ Line mode
|
wenzelm@27949
|
255 |
val line = reader.readLine
|
wenzelm@27949
|
256 |
if (line == null) {
|
wenzelm@27949
|
257 |
reader.close
|
wenzelm@27949
|
258 |
finished = true
|
wenzelm@27949
|
259 |
try_close()
|
wenzelm@27949
|
260 |
}
|
wenzelm@27949
|
261 |
else {
|
wenzelm@27949
|
262 |
val len = line.length
|
wenzelm@27949
|
263 |
// property
|
wenzelm@27949
|
264 |
if (line.endsWith("\u0002,")) {
|
wenzelm@27949
|
265 |
val i = line.indexOf('=')
|
wenzelm@27949
|
266 |
if (i > 0) {
|
wenzelm@27949
|
267 |
val name = line.substring(0, i)
|
wenzelm@27949
|
268 |
val value = line.substring(i + 1, len - 2)
|
wenzelm@27949
|
269 |
if (props == null) props = new Properties
|
wenzelm@27963
|
270 |
if (!props.containsKey(name)) props.setProperty(name, value)
|
wenzelm@27949
|
271 |
}
|
wenzelm@27949
|
272 |
}
|
wenzelm@27949
|
273 |
// last text line
|
wenzelm@27949
|
274 |
else if (line.endsWith("\u0002.")) {
|
wenzelm@27949
|
275 |
result.append(line.substring(0, len - 2))
|
wenzelm@27949
|
276 |
put_result(kind, props, result.toString)
|
wenzelm@27949
|
277 |
result.length = 0
|
wenzelm@27949
|
278 |
kind = Kind.STDOUT
|
wenzelm@27949
|
279 |
}
|
wenzelm@27949
|
280 |
// text line
|
wenzelm@27949
|
281 |
else {
|
wenzelm@27949
|
282 |
result.append(line)
|
wenzelm@27949
|
283 |
result.append('\n')
|
wenzelm@27949
|
284 |
}
|
wenzelm@27949
|
285 |
}
|
wenzelm@27949
|
286 |
//}}}
|
wenzelm@27949
|
287 |
}
|
wenzelm@27963
|
288 |
}
|
wenzelm@27963
|
289 |
catch {
|
wenzelm@27949
|
290 |
case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage)
|
wenzelm@27949
|
291 |
}
|
wenzelm@27949
|
292 |
}
|
wenzelm@27949
|
293 |
put_result(Kind.SYSTEM, null, "Stdout thread terminated")
|
wenzelm@27949
|
294 |
}
|
wenzelm@27949
|
295 |
}
|
wenzelm@27949
|
296 |
|
wenzelm@27949
|
297 |
|
wenzelm@27949
|
298 |
/* stderr */
|
wenzelm@27949
|
299 |
|
wenzelm@27949
|
300 |
private class StderrThread(reader: BufferedReader) extends Thread {
|
wenzelm@27949
|
301 |
override def run() = {
|
wenzelm@27949
|
302 |
var result = new StringBuilder(100)
|
wenzelm@27949
|
303 |
|
wenzelm@27949
|
304 |
var finished = false
|
wenzelm@27949
|
305 |
while (!finished) {
|
wenzelm@27949
|
306 |
try {
|
wenzelm@27949
|
307 |
//{{{
|
wenzelm@27949
|
308 |
var c = -1
|
wenzelm@27949
|
309 |
var done = false
|
wenzelm@27949
|
310 |
while (!done && (result.length == 0 || reader.ready)) {
|
wenzelm@27949
|
311 |
c = reader.read
|
wenzelm@27949
|
312 |
if (c > 0) result.append(c.asInstanceOf[Char])
|
wenzelm@27949
|
313 |
else done = true
|
wenzelm@27949
|
314 |
}
|
wenzelm@27949
|
315 |
if (result.length > 0) {
|
wenzelm@27949
|
316 |
put_result(Kind.STDERR, null, result.toString)
|
wenzelm@27949
|
317 |
result.length = 0
|
wenzelm@27949
|
318 |
}
|
wenzelm@27949
|
319 |
else {
|
wenzelm@27949
|
320 |
reader.close
|
wenzelm@27949
|
321 |
finished = true
|
wenzelm@27949
|
322 |
try_close()
|
wenzelm@27949
|
323 |
}
|
wenzelm@27949
|
324 |
//}}}
|
wenzelm@27963
|
325 |
}
|
wenzelm@27963
|
326 |
catch {
|
wenzelm@27949
|
327 |
case e: IOException => put_result(Kind.SYSTEM, null, "Stderr thread: " + e.getMessage)
|
wenzelm@27949
|
328 |
}
|
wenzelm@27949
|
329 |
}
|
wenzelm@27949
|
330 |
put_result(Kind.SYSTEM, null, "Stderr thread terminated")
|
wenzelm@27949
|
331 |
}
|
wenzelm@27949
|
332 |
}
|
wenzelm@27949
|
333 |
|
wenzelm@27949
|
334 |
|
wenzelm@27949
|
335 |
/* exit */
|
wenzelm@27949
|
336 |
|
wenzelm@27949
|
337 |
private class ExitThread extends Thread {
|
wenzelm@27949
|
338 |
override def run() = {
|
wenzelm@27990
|
339 |
val rc = proc.waitFor()
|
wenzelm@27949
|
340 |
Thread.sleep(300)
|
wenzelm@27949
|
341 |
put_result(Kind.SYSTEM, null, "Exit thread terminated")
|
wenzelm@27949
|
342 |
put_result(Kind.EXIT, null, Integer.toString(rc))
|
wenzelm@27949
|
343 |
}
|
wenzelm@27949
|
344 |
}
|
wenzelm@27949
|
345 |
|
wenzelm@27949
|
346 |
|
wenzelm@27949
|
347 |
|
wenzelm@27949
|
348 |
/** main **/
|
wenzelm@27949
|
349 |
|
wenzelm@27949
|
350 |
{
|
wenzelm@27973
|
351 |
/* exec process */
|
wenzelm@27949
|
352 |
|
wenzelm@27973
|
353 |
try {
|
wenzelm@27973
|
354 |
proc = IsabelleSystem.exec(List(
|
wenzelm@27973
|
355 |
IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args)
|
wenzelm@27973
|
356 |
}
|
wenzelm@27993
|
357 |
catch {
|
wenzelm@27993
|
358 |
case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage)
|
wenzelm@27993
|
359 |
}
|
wenzelm@27963
|
360 |
|
wenzelm@27949
|
361 |
|
wenzelm@27973
|
362 |
/* control process via threads */
|
wenzelm@27949
|
363 |
|
wenzelm@27973
|
364 |
val charset = "UTF-8"
|
wenzelm@27949
|
365 |
new StdinThread(new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, charset))).start
|
wenzelm@27949
|
366 |
new StdoutThread(new BufferedReader(new InputStreamReader(proc.getInputStream, charset))).start
|
wenzelm@27949
|
367 |
new StderrThread(new BufferedReader(new InputStreamReader(proc.getErrorStream, charset))).start
|
wenzelm@27949
|
368 |
new ExitThread().start
|
wenzelm@27949
|
369 |
}
|
wenzelm@27949
|
370 |
|
wenzelm@27949
|
371 |
}
|