author | wenzelm |
Fri, 25 Apr 2014 12:27:18 +0200 | |
changeset 56714 | 061f83259922 |
parent 56703 | 2d0ca179e749 |
child 56784 | 776890e0cf71 |
permissions | -rw-r--r-- |
43283 | 1 |
/* Title: Pure/System/isabelle_process.scala |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
27963 | 3 |
Options: :folding=explicit:collapseFolds=1: |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
4 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
5 |
Isabelle process management -- always reactive due to multi-threaded I/O. |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
6 |
*/ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
7 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
9 |
|
55618 | 10 |
|
56703 | 11 |
import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
12 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
13 |
|
45055
55274f7e306b
explicit option for socket vs. fifo communication;
wenzelm
parents:
45027
diff
changeset
|
14 |
class Isabelle_Process( |
56387 | 15 |
receiver: Prover.Message => Unit = Console.println(_), |
16 |
prover_args: List[String] = Nil) |
|
29192 | 17 |
{ |
56387 | 18 |
/* text and tree data */ |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
19 |
|
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
20 |
def encode(s: String): String = Symbol.encode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
21 |
def decode(s: String): String = Symbol.decode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
22 |
|
56387 | 23 |
val xml_cache = new XML.Cache() |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
24 |
|
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
25 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
26 |
/* output */ |
39573 | 27 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
28 |
private def system_output(text: String) |
39573 | 29 |
{ |
56385 | 30 |
receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) |
39573 | 31 |
} |
32 |
||
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
33 |
private def protocol_output(props: Properties.T, bytes: Bytes) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
34 |
{ |
56385 | 35 |
receiver(new Prover.Protocol_Output(props, bytes)) |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
36 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
37 |
|
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
38 |
private def output(kind: String, props: Properties.T, body: XML.Body) |
39573 | 39 |
{ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
40 |
if (kind == Markup.INIT) system_channel.accepted() |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
41 |
|
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
42 |
val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body)) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
43 |
val reports = Protocol.message_reports(props, body) |
56385 | 44 |
for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg))) |
39573 | 45 |
} |
46 |
||
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
47 |
private def exit_message(rc: Int) |
39573 | 48 |
{ |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
49 |
output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString))) |
39573 | 50 |
} |
51 |
||
52 |
||
56387 | 53 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
54 |
/** process manager **/ |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
55 |
|
56390
8185044353fd
recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
wenzelm
parents:
56387
diff
changeset
|
56 |
def command_line(channel: System_Channel, args: List[String]): List[String] = |
8185044353fd
recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
wenzelm
parents:
56387
diff
changeset
|
57 |
Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: (channel.isabelle_args ::: args) |
8185044353fd
recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
wenzelm
parents:
56387
diff
changeset
|
58 |
|
45158 | 59 |
private val system_channel = System_Channel() |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
60 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
61 |
private val process = |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
62 |
try { |
56390
8185044353fd
recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
wenzelm
parents:
56387
diff
changeset
|
63 |
val cmdline = command_line(system_channel, prover_args) |
48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48020
diff
changeset
|
64 |
new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
65 |
} |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
66 |
catch { case e: IOException => system_channel.accepted(); throw(e) } |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
67 |
|
56387 | 68 |
private val (_, process_result) = |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
69 |
Simple_Thread.future("process_result") { process.join } |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
70 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
71 |
private def terminate_process() |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
72 |
{ |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
73 |
try { process.terminate } |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
74 |
catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) } |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
75 |
} |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
76 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
77 |
private val process_manager = Simple_Thread.fork("process_manager") |
39572 | 78 |
{ |
46548
c54a4a22501c
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
wenzelm
parents:
46121
diff
changeset
|
79 |
val (startup_failed, startup_errors) = |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
80 |
{ |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
81 |
var finished: Option[Boolean] = None |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
82 |
val result = new StringBuilder(100) |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
83 |
while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) { |
46548
c54a4a22501c
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
wenzelm
parents:
46121
diff
changeset
|
84 |
while (finished.isEmpty && process.stderr.ready) { |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
85 |
try { |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
86 |
val c = process.stderr.read |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
87 |
if (c == 2) finished = Some(true) |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
88 |
else result += c.toChar |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
89 |
} |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
90 |
catch { case _: IOException => finished = Some(false) } |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
91 |
} |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
92 |
Thread.sleep(10) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
93 |
} |
39623 | 94 |
(finished.isEmpty || !finished.get, result.toString.trim) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
95 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
96 |
if (startup_errors != "") system_output(startup_errors) |
39572 | 97 |
|
52581 | 98 |
process.stdin.close |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
99 |
if (startup_failed) { |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
100 |
exit_message(127) |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
101 |
Thread.sleep(300) |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
102 |
terminate_process() |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
103 |
process_result.join |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
104 |
} |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
105 |
else { |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
106 |
val (command_stream, message_stream) = system_channel.rendezvous() |
39530
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
107 |
|
56700 | 108 |
command_input_init(command_stream) |
56697 | 109 |
val stdout = physical_output(false) |
110 |
val stderr = physical_output(true) |
|
111 |
val message = message_output(message_stream) |
|
112 |
||
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
113 |
val rc = process_result.join |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
114 |
system_output("process terminated") |
56700 | 115 |
command_input_close() |
56697 | 116 |
for (thread <- List(stdout, stderr, message)) thread.join |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
117 |
system_output("process_manager terminated") |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
118 |
exit_message(rc) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
119 |
} |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
120 |
system_channel.accepted() |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
121 |
} |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
122 |
|
39572 | 123 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
124 |
/* management methods */ |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
125 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
126 |
def join() { process_manager.join() } |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
127 |
|
56617
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
128 |
def interrupt() |
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
129 |
{ |
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
130 |
try { process.interrupt } |
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
131 |
catch { case e: IOException => system_output("Failed to interrupt Isabelle: " + e.getMessage) } |
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
132 |
} |
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
133 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
134 |
def terminate() |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
135 |
{ |
56700 | 136 |
command_input_close() |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
137 |
system_output("Terminating Isabelle process") |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
138 |
terminate_process() |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
139 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
140 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
141 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
142 |
|
56714 | 143 |
/** process streams **/ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
144 |
|
56700 | 145 |
/* command input */ |
146 |
||
147 |
private var command_input: Option[Consumer_Thread[List[Bytes]]] = None |
|
148 |
||
149 |
private def command_input_close(): Unit = command_input.foreach(_.shutdown) |
|
150 |
||
151 |
private def command_input_init(raw_stream: OutputStream) |
|
152 |
{ |
|
153 |
val name = "command_input" |
|
154 |
val stream = new BufferedOutputStream(raw_stream) |
|
155 |
command_input = |
|
156 |
Some( |
|
157 |
Consumer_Thread.fork(name)( |
|
158 |
consume = |
|
159 |
{ |
|
160 |
case chunks => |
|
161 |
try { |
|
162 |
Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream) |
|
163 |
chunks.foreach(_.write(stream)) |
|
164 |
stream.flush |
|
165 |
true |
|
166 |
} |
|
167 |
catch { case e: IOException => system_output(name + ": " + e.getMessage); false } |
|
168 |
}, |
|
169 |
finish = { case () => stream.close; system_output(name + " terminated") } |
|
170 |
) |
|
171 |
) |
|
172 |
} |
|
173 |
||
174 |
||
46773 | 175 |
/* physical output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
176 |
|
56697 | 177 |
private def physical_output(err: Boolean): Thread = |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
178 |
{ |
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
179 |
val (name, reader, markup) = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
180 |
if (err) ("standard_error", process.stderr, Markup.STDERR) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
181 |
else ("standard_output", process.stdout, Markup.STDOUT) |
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
182 |
|
56697 | 183 |
Simple_Thread.fork(name) { |
46769 | 184 |
try { |
185 |
var result = new StringBuilder(100) |
|
186 |
var finished = false |
|
187 |
while (!finished) { |
|
28045 | 188 |
//{{{ |
189 |
var c = -1 |
|
190 |
var done = false |
|
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
191 |
while (!done && (result.length == 0 || reader.ready)) { |
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
192 |
c = reader.read |
28045 | 193 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
194 |
else done = true |
|
195 |
} |
|
196 |
if (result.length > 0) { |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
197 |
output(markup, Nil, List(XML.Text(decode(result.toString)))) |
28045 | 198 |
result.length = 0 |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
199 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
200 |
else { |
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
201 |
reader.close |
28045 | 202 |
finished = true |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
203 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
204 |
//}}} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
205 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
206 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
207 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
208 |
system_output(name + " terminated") |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
209 |
} |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
210 |
} |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
211 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
212 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
213 |
/* message output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
214 |
|
56697 | 215 |
private def message_output(stream: InputStream): Thread = |
39526 | 216 |
{ |
217 |
class EOF extends Exception |
|
218 |
class Protocol_Error(msg: String) extends Exception(msg) |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
219 |
|
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
220 |
val name = "message_output" |
56697 | 221 |
Simple_Thread.fork(name) { |
34100 | 222 |
val default_buffer = new Array[Byte](65536) |
223 |
var c = -1 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
224 |
|
52799 | 225 |
def read_int(): Int = |
226 |
//{{{ |
|
34100 | 227 |
{ |
228 |
var n = 0 |
|
229 |
c = stream.read |
|
39526 | 230 |
if (c == -1) throw new EOF |
34100 | 231 |
while (48 <= c && c <= 57) { |
232 |
n = 10 * n + (c - 48) |
|
233 |
c = stream.read |
|
234 |
} |
|
52799 | 235 |
if (c != 10) |
236 |
throw new Protocol_Error("malformed header: expected integer followed by newline") |
|
237 |
else n |
|
238 |
} |
|
239 |
//}}} |
|
34100 | 240 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
241 |
def read_chunk_bytes(): (Array[Byte], Int) = |
52799 | 242 |
//{{{ |
243 |
{ |
|
244 |
val n = read_int() |
|
34100 | 245 |
val buf = |
246 |
if (n <= default_buffer.size) default_buffer |
|
247 |
else new Array[Byte](n) |
|
248 |
||
249 |
var i = 0 |
|
250 |
var m = 0 |
|
251 |
do { |
|
252 |
m = stream.read(buf, i, n - i) |
|
39731
5cb0d7b0d601
bulk read: observe EOF protocol more carefully -- 0 counts as successful read;
wenzelm
parents:
39632
diff
changeset
|
253 |
if (m != -1) i += m |
52799 | 254 |
} |
255 |
while (m != -1 && n > i) |
|
34100 | 256 |
|
52799 | 257 |
if (i != n) |
258 |
throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)") |
|
34100 | 259 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
260 |
(buf, n) |
34100 | 261 |
} |
52799 | 262 |
//}}} |
34100 | 263 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
264 |
def read_chunk(): XML.Body = |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
265 |
{ |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
266 |
val (buf, n) = read_chunk_bytes() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
267 |
YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n)) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
268 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
269 |
|
46769 | 270 |
try { |
271 |
do { |
|
272 |
try { |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
273 |
val header = read_chunk() |
46769 | 274 |
header match { |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49445
diff
changeset
|
275 |
case List(XML.Elem(Markup(name, props), Nil)) => |
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49445
diff
changeset
|
276 |
val kind = name.intern |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
277 |
if (kind == Markup.PROTOCOL) { |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
278 |
val (buf, n) = read_chunk_bytes() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
279 |
protocol_output(props, Bytes(buf, 0, n)) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
280 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
281 |
else { |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
282 |
val body = read_chunk() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
283 |
output(kind, props, body) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
284 |
} |
46769 | 285 |
case _ => |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
286 |
read_chunk() |
46769 | 287 |
throw new Protocol_Error("bad header: " + header.toString) |
288 |
} |
|
28063 | 289 |
} |
46769 | 290 |
catch { case _: EOF => } |
52799 | 291 |
} |
292 |
while (c != -1) |
|
46769 | 293 |
} |
294 |
catch { |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
295 |
case e: IOException => system_output("Cannot read message:\n" + e.getMessage) |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
296 |
case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage) |
46769 | 297 |
} |
34100 | 298 |
stream.close |
299 |
||
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
300 |
system_output(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
301 |
} |
39526 | 302 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
303 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
304 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
305 |
|
56387 | 306 |
/** protocol commands **/ |
307 |
||
308 |
def protocol_command_bytes(name: String, args: Bytes*): Unit = |
|
56700 | 309 |
command_input match { |
310 |
case Some(thread) => thread.send(Bytes(name) :: args.toList) |
|
311 |
case None => error("Uninitialized command input thread") |
|
312 |
} |
|
38372
e753f71b6b34
added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
wenzelm
parents:
38270
diff
changeset
|
313 |
|
52582 | 314 |
def protocol_command(name: String, args: String*) |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
315 |
{ |
56385 | 316 |
receiver(new Prover.Input(name, args.toList)) |
56387 | 317 |
protocol_command_bytes(name, args.map(Bytes(_)): _*) |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
318 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
319 |
} |