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