wenzelm@30174
|
1 |
/* Title: Pure/System/isabelle_process.ML
|
wenzelm@27949
|
2 |
Author: Makarius
|
wenzelm@27963
|
3 |
Options: :folding=explicit:collapseFolds=1:
|
wenzelm@27949
|
4 |
|
wenzelm@27949
|
5 |
Isabelle process management -- always reactive due to multi-threaded I/O.
|
wenzelm@27949
|
6 |
*/
|
wenzelm@27949
|
7 |
|
wenzelm@27949
|
8 |
package isabelle
|
wenzelm@27949
|
9 |
|
wenzelm@27955
|
10 |
import java.util.concurrent.LinkedBlockingQueue
|
wenzelm@28045
|
11 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
|
wenzelm@28056
|
12 |
InputStream, OutputStream, IOException}
|
wenzelm@27949
|
13 |
|
wenzelm@32485
|
14 |
import scala.actors.Actor
|
wenzelm@32485
|
15 |
import Actor._
|
wenzelm@27949
|
16 |
|
wenzelm@27973
|
17 |
|
wenzelm@32485
|
18 |
object Isabelle_Process
|
wenzelm@32485
|
19 |
{
|
wenzelm@27949
|
20 |
/* results */
|
wenzelm@27949
|
21 |
|
wenzelm@27949
|
22 |
object Kind extends Enumeration {
|
wenzelm@28344
|
23 |
//{{{ values and codes
|
wenzelm@28344
|
24 |
// internal system notification
|
wenzelm@28344
|
25 |
val SYSTEM = Value("SYSTEM")
|
wenzelm@27949
|
26 |
// Posix channels/events
|
wenzelm@27949
|
27 |
val STDIN = Value("STDIN")
|
wenzelm@27949
|
28 |
val STDOUT = Value("STDOUT")
|
wenzelm@27949
|
29 |
val SIGNAL = Value("SIGNAL")
|
wenzelm@27949
|
30 |
val EXIT = Value("EXIT")
|
wenzelm@27949
|
31 |
// Isabelle messages
|
wenzelm@28344
|
32 |
val INIT = Value("INIT")
|
wenzelm@28344
|
33 |
val STATUS = Value("STATUS")
|
wenzelm@27949
|
34 |
val WRITELN = Value("WRITELN")
|
wenzelm@27949
|
35 |
val PRIORITY = Value("PRIORITY")
|
wenzelm@27949
|
36 |
val TRACING = Value("TRACING")
|
wenzelm@27949
|
37 |
val WARNING = Value("WARNING")
|
wenzelm@27949
|
38 |
val ERROR = Value("ERROR")
|
wenzelm@27949
|
39 |
val DEBUG = Value("DEBUG")
|
wenzelm@28344
|
40 |
// messages codes
|
wenzelm@28344
|
41 |
val code = Map(
|
wenzelm@28344
|
42 |
('A' : Int) -> Kind.INIT,
|
wenzelm@28344
|
43 |
('B' : Int) -> Kind.STATUS,
|
wenzelm@28344
|
44 |
('C' : Int) -> Kind.WRITELN,
|
wenzelm@28344
|
45 |
('D' : Int) -> Kind.PRIORITY,
|
wenzelm@28344
|
46 |
('E' : Int) -> Kind.TRACING,
|
wenzelm@28344
|
47 |
('F' : Int) -> Kind.WARNING,
|
wenzelm@28344
|
48 |
('G' : Int) -> Kind.ERROR,
|
wenzelm@28344
|
49 |
('H' : Int) -> Kind.DEBUG,
|
wenzelm@28344
|
50 |
('0' : Int) -> Kind.SYSTEM,
|
wenzelm@28344
|
51 |
('1' : Int) -> Kind.STDIN,
|
wenzelm@28344
|
52 |
('2' : Int) -> Kind.STDOUT,
|
wenzelm@28344
|
53 |
('3' : Int) -> Kind.SIGNAL,
|
wenzelm@28344
|
54 |
('4' : Int) -> Kind.EXIT)
|
wenzelm@29522
|
55 |
// message markup
|
wenzelm@29522
|
56 |
val markup = Map(
|
wenzelm@29522
|
57 |
Kind.INIT -> Markup.INIT,
|
wenzelm@29522
|
58 |
Kind.STATUS -> Markup.STATUS,
|
wenzelm@29522
|
59 |
Kind.WRITELN -> Markup.WRITELN,
|
wenzelm@29522
|
60 |
Kind.PRIORITY -> Markup.PRIORITY,
|
wenzelm@29522
|
61 |
Kind.TRACING -> Markup.TRACING,
|
wenzelm@29522
|
62 |
Kind.WARNING -> Markup.WARNING,
|
wenzelm@29522
|
63 |
Kind.ERROR -> Markup.ERROR,
|
wenzelm@29522
|
64 |
Kind.DEBUG -> Markup.DEBUG,
|
wenzelm@29522
|
65 |
Kind.SYSTEM -> Markup.SYSTEM,
|
wenzelm@29522
|
66 |
Kind.STDIN -> Markup.STDIN,
|
wenzelm@29522
|
67 |
Kind.STDOUT -> Markup.STDOUT,
|
wenzelm@29522
|
68 |
Kind.SIGNAL -> Markup.SIGNAL,
|
wenzelm@29522
|
69 |
Kind.EXIT -> Markup.EXIT)
|
wenzelm@27949
|
70 |
//}}}
|
wenzelm@27949
|
71 |
def is_raw(kind: Value) =
|
wenzelm@28045
|
72 |
kind == STDOUT
|
wenzelm@27990
|
73 |
def is_control(kind: Value) =
|
wenzelm@28344
|
74 |
kind == SYSTEM ||
|
wenzelm@27990
|
75 |
kind == SIGNAL ||
|
wenzelm@28344
|
76 |
kind == EXIT
|
wenzelm@27949
|
77 |
def is_system(kind: Value) =
|
wenzelm@28344
|
78 |
kind == SYSTEM ||
|
wenzelm@27949
|
79 |
kind == STDIN ||
|
wenzelm@27949
|
80 |
kind == SIGNAL ||
|
wenzelm@27949
|
81 |
kind == EXIT ||
|
wenzelm@28498
|
82 |
kind == STATUS
|
wenzelm@27949
|
83 |
}
|
wenzelm@27949
|
84 |
|
wenzelm@34106
|
85 |
class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
|
wenzelm@34106
|
86 |
{
|
wenzelm@34106
|
87 |
def message = XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(kind)) :: props, body)
|
wenzelm@34106
|
88 |
|
wenzelm@34106
|
89 |
override def toString: String =
|
wenzelm@34106
|
90 |
{
|
wenzelm@29522
|
91 |
val res =
|
wenzelm@34106
|
92 |
if (kind == Kind.STATUS) body.map(_.toString).mkString
|
wenzelm@34106
|
93 |
else body.map(XML.content(_).mkString).mkString
|
wenzelm@29572
|
94 |
if (props.isEmpty)
|
wenzelm@29572
|
95 |
kind.toString + " [[" + res + "]]"
|
wenzelm@29572
|
96 |
else
|
wenzelm@29572
|
97 |
kind.toString + " " +
|
wenzelm@29572
|
98 |
(for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
|
wenzelm@27949
|
99 |
}
|
wenzelm@29192
|
100 |
def is_raw = Kind.is_raw(kind)
|
wenzelm@29192
|
101 |
def is_control = Kind.is_control(kind)
|
wenzelm@29192
|
102 |
def is_system = Kind.is_system(kind)
|
wenzelm@34114
|
103 |
|
wenzelm@34126
|
104 |
def cache(c: XML.Cache): Result =
|
wenzelm@34126
|
105 |
new Result(kind, c.cache_props(props), c.cache_trees(body))
|
wenzelm@27973
|
106 |
}
|
wenzelm@27973
|
107 |
}
|
wenzelm@27973
|
108 |
|
wenzelm@27973
|
109 |
|
wenzelm@34106
|
110 |
class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*)
|
wenzelm@29192
|
111 |
{
|
wenzelm@31800
|
112 |
import Isabelle_Process._
|
wenzelm@29194
|
113 |
|
wenzelm@27973
|
114 |
|
wenzelm@29192
|
115 |
/* demo constructor */
|
wenzelm@27973
|
116 |
|
wenzelm@29192
|
117 |
def this(args: String*) =
|
wenzelm@32485
|
118 |
this(new Isabelle_System,
|
wenzelm@32485
|
119 |
new Actor { def act = loop { react { case res => Console.println(res) } } }.start, args: _*)
|
wenzelm@29174
|
120 |
|
wenzelm@29174
|
121 |
|
wenzelm@27973
|
122 |
/* process information */
|
wenzelm@27973
|
123 |
|
wenzelm@29648
|
124 |
@volatile private var proc: Process = null
|
wenzelm@29648
|
125 |
@volatile private var closing = false
|
wenzelm@29648
|
126 |
@volatile private var pid: String = null
|
wenzelm@29648
|
127 |
@volatile private var the_session: String = null
|
wenzelm@29572
|
128 |
def session = the_session
|
wenzelm@27973
|
129 |
|
wenzelm@27973
|
130 |
|
wenzelm@27973
|
131 |
/* results */
|
wenzelm@27949
|
132 |
|
wenzelm@34106
|
133 |
private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree])
|
wenzelm@29572
|
134 |
{
|
wenzelm@29572
|
135 |
if (kind == Kind.INIT) {
|
wenzelm@29572
|
136 |
val map = Map(props: _*)
|
wenzelm@29572
|
137 |
if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
|
wenzelm@29572
|
138 |
if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
|
wenzelm@27963
|
139 |
}
|
wenzelm@34106
|
140 |
receiver ! new Result(kind, props, body)
|
wenzelm@34106
|
141 |
}
|
wenzelm@34106
|
142 |
|
wenzelm@34106
|
143 |
private def put_result(kind: Kind.Value, text: String)
|
wenzelm@34106
|
144 |
{
|
wenzelm@34106
|
145 |
put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
|
wenzelm@27992
|
146 |
}
|
wenzelm@27992
|
147 |
|
wenzelm@27973
|
148 |
|
wenzelm@27973
|
149 |
/* signals */
|
wenzelm@27973
|
150 |
|
wenzelm@27973
|
151 |
def interrupt() = synchronized {
|
wenzelm@27993
|
152 |
if (proc == null) error("Cannot interrupt Isabelle: no process")
|
wenzelm@34106
|
153 |
if (pid == null) put_result(Kind.SYSTEM, "Cannot interrupt: unknown pid")
|
wenzelm@27973
|
154 |
else {
|
wenzelm@27973
|
155 |
try {
|
wenzelm@34106
|
156 |
if (system.execute(true, "kill", "-INT", pid).waitFor == 0)
|
wenzelm@34106
|
157 |
put_result(Kind.SIGNAL, "INT")
|
wenzelm@27990
|
158 |
else
|
wenzelm@34106
|
159 |
put_result(Kind.SYSTEM, "Cannot interrupt: kill command failed")
|
wenzelm@27973
|
160 |
}
|
wenzelm@27993
|
161 |
catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
|
wenzelm@27973
|
162 |
}
|
wenzelm@27973
|
163 |
}
|
wenzelm@27973
|
164 |
|
wenzelm@27973
|
165 |
def kill() = synchronized {
|
wenzelm@27993
|
166 |
if (proc == 0) error("Cannot kill Isabelle: no process")
|
wenzelm@27973
|
167 |
else {
|
wenzelm@27973
|
168 |
try_close()
|
wenzelm@27990
|
169 |
Thread.sleep(500)
|
wenzelm@34106
|
170 |
put_result(Kind.SIGNAL, "KILL")
|
wenzelm@27973
|
171 |
proc.destroy
|
wenzelm@27973
|
172 |
proc = null
|
wenzelm@27990
|
173 |
pid = null
|
wenzelm@27973
|
174 |
}
|
wenzelm@27973
|
175 |
}
|
wenzelm@27973
|
176 |
|
wenzelm@27949
|
177 |
|
wenzelm@27949
|
178 |
/* output being piped into the process */
|
wenzelm@27949
|
179 |
|
wenzelm@27990
|
180 |
private val output = new LinkedBlockingQueue[String]
|
wenzelm@27949
|
181 |
|
wenzelm@28045
|
182 |
private def output_raw(text: String) = synchronized {
|
wenzelm@27993
|
183 |
if (proc == null) error("Cannot output to Isabelle: no process")
|
wenzelm@27993
|
184 |
if (closing) error("Cannot output to Isabelle: already closing")
|
wenzelm@27955
|
185 |
output.put(text)
|
wenzelm@27949
|
186 |
}
|
wenzelm@27949
|
187 |
|
wenzelm@28303
|
188 |
def output_sync(text: String) =
|
wenzelm@28045
|
189 |
output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
|
wenzelm@27949
|
190 |
|
wenzelm@27963
|
191 |
|
wenzelm@27963
|
192 |
def command(text: String) =
|
wenzelm@32448
|
193 |
output_sync("Isabelle.command " + Isabelle_Syntax.encode_string(text))
|
wenzelm@27949
|
194 |
|
wenzelm@29572
|
195 |
def command(props: List[(String, String)], text: String) =
|
wenzelm@32448
|
196 |
output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
|
wenzelm@32448
|
197 |
Isabelle_Syntax.encode_string(text))
|
wenzelm@27949
|
198 |
|
wenzelm@27963
|
199 |
def ML(text: String) =
|
wenzelm@32448
|
200 |
output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
|
wenzelm@27949
|
201 |
|
wenzelm@27949
|
202 |
def close() = synchronized { // FIXME watchdog/timeout
|
wenzelm@27949
|
203 |
output_raw("\u0000")
|
wenzelm@27949
|
204 |
closing = true
|
wenzelm@27949
|
205 |
}
|
wenzelm@27949
|
206 |
|
wenzelm@27949
|
207 |
def try_close() = synchronized {
|
wenzelm@27949
|
208 |
if (proc != null && !closing) {
|
wenzelm@27949
|
209 |
try { close() }
|
wenzelm@27993
|
210 |
catch { case _: RuntimeException => }
|
wenzelm@27949
|
211 |
}
|
wenzelm@27949
|
212 |
}
|
wenzelm@27949
|
213 |
|
wenzelm@27949
|
214 |
|
wenzelm@27949
|
215 |
/* stdin */
|
wenzelm@27949
|
216 |
|
wenzelm@28045
|
217 |
private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
|
wenzelm@27949
|
218 |
override def run() = {
|
wenzelm@31800
|
219 |
val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Isabelle_System.charset))
|
wenzelm@27949
|
220 |
var finished = false
|
wenzelm@27949
|
221 |
while (!finished) {
|
wenzelm@27949
|
222 |
try {
|
wenzelm@27949
|
223 |
//{{{
|
wenzelm@27955
|
224 |
val s = output.take
|
wenzelm@27949
|
225 |
if (s == "\u0000") {
|
wenzelm@27949
|
226 |
writer.close
|
wenzelm@27949
|
227 |
finished = true
|
wenzelm@27949
|
228 |
}
|
wenzelm@27949
|
229 |
else {
|
wenzelm@34106
|
230 |
put_result(Kind.STDIN, s)
|
wenzelm@27949
|
231 |
writer.write(s)
|
wenzelm@27949
|
232 |
writer.flush
|
wenzelm@27949
|
233 |
}
|
wenzelm@27949
|
234 |
//}}}
|
wenzelm@27949
|
235 |
}
|
wenzelm@27949
|
236 |
catch {
|
wenzelm@34106
|
237 |
case e: IOException => put_result(Kind.SYSTEM, "Stdin thread: " + e.getMessage)
|
wenzelm@27949
|
238 |
}
|
wenzelm@27949
|
239 |
}
|
wenzelm@34106
|
240 |
put_result(Kind.SYSTEM, "Stdin thread terminated")
|
wenzelm@27949
|
241 |
}
|
wenzelm@27949
|
242 |
}
|
wenzelm@27949
|
243 |
|
wenzelm@27949
|
244 |
|
wenzelm@27949
|
245 |
/* stdout */
|
wenzelm@27949
|
246 |
|
wenzelm@28045
|
247 |
private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
|
wenzelm@27949
|
248 |
override def run() = {
|
wenzelm@31800
|
249 |
val reader = new BufferedReader(new InputStreamReader(in_stream, Isabelle_System.charset))
|
wenzelm@27949
|
250 |
var result = new StringBuilder(100)
|
wenzelm@27949
|
251 |
|
wenzelm@27949
|
252 |
var finished = false
|
wenzelm@27949
|
253 |
while (!finished) {
|
wenzelm@27949
|
254 |
try {
|
wenzelm@27949
|
255 |
//{{{
|
wenzelm@27949
|
256 |
var c = -1
|
wenzelm@27949
|
257 |
var done = false
|
wenzelm@27949
|
258 |
while (!done && (result.length == 0 || reader.ready)) {
|
wenzelm@27949
|
259 |
c = reader.read
|
wenzelm@28045
|
260 |
if (c >= 0) result.append(c.asInstanceOf[Char])
|
wenzelm@27949
|
261 |
else done = true
|
wenzelm@27949
|
262 |
}
|
wenzelm@27949
|
263 |
if (result.length > 0) {
|
wenzelm@34106
|
264 |
put_result(Kind.STDOUT, result.toString)
|
wenzelm@27949
|
265 |
result.length = 0
|
wenzelm@27949
|
266 |
}
|
wenzelm@27949
|
267 |
else {
|
wenzelm@27949
|
268 |
reader.close
|
wenzelm@27949
|
269 |
finished = true
|
wenzelm@27949
|
270 |
try_close()
|
wenzelm@27949
|
271 |
}
|
wenzelm@27949
|
272 |
//}}}
|
wenzelm@27963
|
273 |
}
|
wenzelm@27963
|
274 |
catch {
|
wenzelm@34106
|
275 |
case e: IOException => put_result(Kind.SYSTEM, "Stdout thread: " + e.getMessage)
|
wenzelm@27949
|
276 |
}
|
wenzelm@27949
|
277 |
}
|
wenzelm@34106
|
278 |
put_result(Kind.SYSTEM, "Stdout thread terminated")
|
wenzelm@27949
|
279 |
}
|
wenzelm@27949
|
280 |
}
|
wenzelm@27949
|
281 |
|
wenzelm@27949
|
282 |
|
wenzelm@28045
|
283 |
/* messages */
|
wenzelm@27949
|
284 |
|
wenzelm@34106
|
285 |
private class MessageThread(fifo: String) extends Thread("isabelle: messages")
|
wenzelm@34106
|
286 |
{
|
wenzelm@34106
|
287 |
private class Protocol_Error(msg: String) extends Exception(msg)
|
wenzelm@34106
|
288 |
override def run()
|
wenzelm@34106
|
289 |
{
|
wenzelm@34106
|
290 |
val stream = system.fifo_stream(fifo)
|
wenzelm@34106
|
291 |
val default_buffer = new Array[Byte](65536)
|
wenzelm@34106
|
292 |
var c = -1
|
wenzelm@28045
|
293 |
|
wenzelm@34106
|
294 |
def read_chunk(): List[XML.Tree] =
|
wenzelm@34106
|
295 |
{
|
wenzelm@34106
|
296 |
//{{{
|
wenzelm@34106
|
297 |
// chunk size
|
wenzelm@34106
|
298 |
var n = 0
|
wenzelm@34106
|
299 |
c = stream.read
|
wenzelm@34106
|
300 |
while (48 <= c && c <= 57) {
|
wenzelm@34106
|
301 |
n = 10 * n + (c - 48)
|
wenzelm@34106
|
302 |
c = stream.read
|
wenzelm@34106
|
303 |
}
|
wenzelm@34106
|
304 |
if (c != 10) throw new Protocol_Error("bad message chunk header")
|
wenzelm@34106
|
305 |
|
wenzelm@34106
|
306 |
// chunk content
|
wenzelm@34106
|
307 |
val buf =
|
wenzelm@34106
|
308 |
if (n <= default_buffer.size) default_buffer
|
wenzelm@34106
|
309 |
else new Array[Byte](n)
|
wenzelm@34106
|
310 |
|
wenzelm@34106
|
311 |
var i = 0
|
wenzelm@34106
|
312 |
var m = 0
|
wenzelm@34106
|
313 |
do {
|
wenzelm@34106
|
314 |
m = stream.read(buf, i, n - i)
|
wenzelm@34106
|
315 |
i += m
|
wenzelm@34106
|
316 |
} while (m > 0 && n > i)
|
wenzelm@34106
|
317 |
|
wenzelm@34106
|
318 |
if (i != n) throw new Protocol_Error("bad message chunk content")
|
wenzelm@34106
|
319 |
|
wenzelm@34106
|
320 |
YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
|
wenzelm@34106
|
321 |
//}}}
|
wenzelm@34106
|
322 |
}
|
wenzelm@34106
|
323 |
|
wenzelm@34106
|
324 |
do {
|
wenzelm@28045
|
325 |
try {
|
wenzelm@34106
|
326 |
//{{{
|
wenzelm@34106
|
327 |
c = stream.read
|
wenzelm@34106
|
328 |
var non_sync = 0
|
wenzelm@34106
|
329 |
while (c >= 0 && c != 2) {
|
wenzelm@34106
|
330 |
non_sync += 1
|
wenzelm@34106
|
331 |
c = stream.read
|
wenzelm@34106
|
332 |
}
|
wenzelm@34106
|
333 |
if (non_sync > 0)
|
wenzelm@34106
|
334 |
throw new Protocol_Error("lost synchronization -- skipping " + non_sync + " bytes")
|
wenzelm@34106
|
335 |
if (c == 2) {
|
wenzelm@34106
|
336 |
val header = read_chunk()
|
wenzelm@34106
|
337 |
val body = read_chunk()
|
wenzelm@34106
|
338 |
header match {
|
wenzelm@34106
|
339 |
case List(XML.Elem(name, props, Nil))
|
wenzelm@34106
|
340 |
if name.size == 1 && Kind.code.isDefinedAt(name(0)) =>
|
wenzelm@34106
|
341 |
put_result(Kind.code(name(0)), props, body)
|
wenzelm@34106
|
342 |
case _ => throw new Protocol_Error("bad header: " + header.toString)
|
wenzelm@28063
|
343 |
}
|
wenzelm@28063
|
344 |
}
|
wenzelm@34106
|
345 |
//}}}
|
wenzelm@28045
|
346 |
}
|
wenzelm@28063
|
347 |
catch {
|
wenzelm@34106
|
348 |
case e: IOException =>
|
wenzelm@34106
|
349 |
put_result(Kind.SYSTEM, "Cannot read message:\n" + e.getMessage)
|
wenzelm@34106
|
350 |
case e: Protocol_Error =>
|
wenzelm@34106
|
351 |
put_result(Kind.SYSTEM, "Malformed message:\n" + e.getMessage)
|
wenzelm@28063
|
352 |
}
|
wenzelm@34106
|
353 |
} while (c != -1)
|
wenzelm@34106
|
354 |
stream.close
|
wenzelm@34106
|
355 |
try_close()
|
wenzelm@34106
|
356 |
|
wenzelm@34106
|
357 |
put_result(Kind.SYSTEM, "Message thread terminated")
|
wenzelm@27949
|
358 |
}
|
wenzelm@27949
|
359 |
}
|
wenzelm@27949
|
360 |
|
wenzelm@27949
|
361 |
|
wenzelm@29192
|
362 |
|
wenzelm@27949
|
363 |
/** main **/
|
wenzelm@27949
|
364 |
|
wenzelm@27949
|
365 |
{
|
wenzelm@28497
|
366 |
/* isabelle version */
|
wenzelm@28497
|
367 |
|
wenzelm@28497
|
368 |
{
|
wenzelm@34106
|
369 |
val (msg, rc) = system.isabelle_tool("version")
|
wenzelm@28497
|
370 |
if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
|
wenzelm@34106
|
371 |
put_result(Kind.SYSTEM, msg)
|
wenzelm@28497
|
372 |
}
|
wenzelm@28497
|
373 |
|
wenzelm@28045
|
374 |
|
wenzelm@29192
|
375 |
/* messages */
|
wenzelm@28045
|
376 |
|
wenzelm@34106
|
377 |
val message_fifo = system.mk_fifo()
|
wenzelm@34106
|
378 |
def rm_fifo() = system.rm_fifo(message_fifo)
|
wenzelm@28045
|
379 |
|
wenzelm@28063
|
380 |
val message_thread = new MessageThread(message_fifo)
|
wenzelm@28063
|
381 |
message_thread.start
|
wenzelm@28045
|
382 |
|
wenzelm@28045
|
383 |
|
wenzelm@27973
|
384 |
/* exec process */
|
wenzelm@27949
|
385 |
|
wenzelm@27973
|
386 |
try {
|
wenzelm@34106
|
387 |
val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
|
wenzelm@34106
|
388 |
proc = system.execute(true, cmdline: _*)
|
wenzelm@27973
|
389 |
}
|
wenzelm@27993
|
390 |
catch {
|
wenzelm@28063
|
391 |
case e: IOException =>
|
wenzelm@28063
|
392 |
rm_fifo()
|
wenzelm@28063
|
393 |
error("Failed to execute Isabelle process: " + e.getMessage)
|
wenzelm@27993
|
394 |
}
|
wenzelm@27963
|
395 |
|
wenzelm@27949
|
396 |
|
wenzelm@28045
|
397 |
/* stdin/stdout */
|
wenzelm@27949
|
398 |
|
wenzelm@28045
|
399 |
new StdinThread(proc.getOutputStream).start
|
wenzelm@28045
|
400 |
new StdoutThread(proc.getInputStream).start
|
wenzelm@28045
|
401 |
|
wenzelm@28045
|
402 |
|
wenzelm@28045
|
403 |
/* exit */
|
wenzelm@28045
|
404 |
|
wenzelm@28063
|
405 |
new Thread("isabelle: exit") {
|
wenzelm@28045
|
406 |
override def run() = {
|
wenzelm@28045
|
407 |
val rc = proc.waitFor()
|
wenzelm@28045
|
408 |
Thread.sleep(300)
|
wenzelm@34106
|
409 |
put_result(Kind.SYSTEM, "Exit thread terminated")
|
wenzelm@34106
|
410 |
put_result(Kind.EXIT, rc.toString)
|
wenzelm@28063
|
411 |
rm_fifo()
|
wenzelm@28045
|
412 |
}
|
wenzelm@28063
|
413 |
}.start
|
wenzelm@28063
|
414 |
|
wenzelm@27949
|
415 |
}
|
wenzelm@27949
|
416 |
}
|