author | wenzelm |
Thu, 24 Apr 2014 13:54:45 +0200 | |
changeset 56697 | 76b38be47feb |
parent 56617 | c00646996701 |
child 56700 | c84bf6f63dfe |
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 |
|
27955
4c32c5e75eca
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents:
27949
diff
changeset
|
11 |
import java.util.concurrent.LinkedBlockingQueue |
28045 | 12 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
13 |
InputStream, OutputStream, BufferedOutputStream, IOException} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
14 |
|
32474
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
15 |
import scala.actors.Actor |
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
16 |
import Actor._ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
17 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
18 |
|
45055
55274f7e306b
explicit option for socket vs. fifo communication;
wenzelm
parents:
45027
diff
changeset
|
19 |
class Isabelle_Process( |
56387 | 20 |
receiver: Prover.Message => Unit = Console.println(_), |
21 |
prover_args: List[String] = Nil) |
|
29192 | 22 |
{ |
56387 | 23 |
/* text and tree data */ |
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 |
def encode(s: String): String = Symbol.encode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
26 |
def decode(s: String): String = Symbol.decode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
27 |
|
56387 | 28 |
val xml_cache = new XML.Cache() |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
29 |
|
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
30 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
31 |
/* output */ |
39573 | 32 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
33 |
private def system_output(text: String) |
39573 | 34 |
{ |
56385 | 35 |
receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) |
39573 | 36 |
} |
37 |
||
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
38 |
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
|
39 |
{ |
56385 | 40 |
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
|
41 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
42 |
|
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
43 |
private def output(kind: String, props: Properties.T, body: XML.Body) |
39573 | 44 |
{ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
45 |
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
|
46 |
|
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
47 |
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
|
48 |
val reports = Protocol.message_reports(props, body) |
56385 | 49 |
for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg))) |
39573 | 50 |
} |
51 |
||
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
52 |
private def exit_message(rc: Int) |
39573 | 53 |
{ |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
54 |
output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString))) |
39573 | 55 |
} |
56 |
||
57 |
||
52581 | 58 |
/* command input actor */ |
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
|
59 |
|
56697 | 60 |
@volatile private var command_input: (Thread, Actor) = null |
61 |
||
54440 | 62 |
private case class Input_Chunks(chunks: List[Bytes]) |
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
|
63 |
|
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
|
64 |
private case object Close |
56697 | 65 |
private def close_input() |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
66 |
{ |
56697 | 67 |
if (command_input != null && command_input._1.isAlive) { |
68 |
command_input._2 ! Close |
|
69 |
command_input._1.join |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
70 |
} |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
71 |
} |
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
|
72 |
|
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
|
73 |
|
56387 | 74 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
75 |
/** 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
|
76 |
|
56390
8185044353fd
recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
wenzelm
parents:
56387
diff
changeset
|
77 |
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
|
78 |
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
|
79 |
|
45158 | 80 |
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
|
81 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
82 |
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
|
83 |
try { |
56390
8185044353fd
recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
wenzelm
parents:
56387
diff
changeset
|
84 |
val cmdline = command_line(system_channel, prover_args) |
48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48020
diff
changeset
|
85 |
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
|
86 |
} |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
87 |
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
|
88 |
|
56387 | 89 |
private val (_, process_result) = |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
90 |
Simple_Thread.future("process_result") { process.join } |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
91 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
92 |
private def terminate_process() |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
93 |
{ |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
94 |
try { process.terminate } |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
95 |
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
|
96 |
} |
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
|
97 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
98 |
private val process_manager = Simple_Thread.fork("process_manager") |
39572 | 99 |
{ |
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
|
100 |
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
|
101 |
{ |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
102 |
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
|
103 |
val result = new StringBuilder(100) |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
104 |
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
|
105 |
while (finished.isEmpty && process.stderr.ready) { |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
106 |
try { |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
107 |
val c = process.stderr.read |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
108 |
if (c == 2) finished = Some(true) |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
109 |
else result += c.toChar |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
110 |
} |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
111 |
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
|
112 |
} |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
113 |
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
|
114 |
} |
39623 | 115 |
(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
|
116 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
117 |
if (startup_errors != "") system_output(startup_errors) |
39572 | 118 |
|
52581 | 119 |
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
|
120 |
if (startup_failed) { |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
121 |
exit_message(127) |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
122 |
Thread.sleep(300) |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
123 |
terminate_process() |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
124 |
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
|
125 |
} |
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
|
126 |
else { |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
127 |
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
|
128 |
|
56697 | 129 |
val stdout = physical_output(false) |
130 |
val stderr = physical_output(true) |
|
131 |
val message = message_output(message_stream) |
|
132 |
||
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
133 |
command_input = input_actor(command_stream) |
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
|
134 |
|
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
135 |
val rc = process_result.join |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
136 |
system_output("process terminated") |
56697 | 137 |
close_input() |
138 |
for (thread <- List(stdout, stderr, message)) thread.join |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
139 |
system_output("process_manager terminated") |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
140 |
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
|
141 |
} |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
142 |
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
|
143 |
} |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
144 |
|
39572 | 145 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
146 |
/* management methods */ |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
147 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
148 |
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
|
149 |
|
56617
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
150 |
def interrupt() |
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
151 |
{ |
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
152 |
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
|
153 |
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
|
154 |
} |
c00646996701
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
wenzelm
parents:
56390
diff
changeset
|
155 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
156 |
def terminate() |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
157 |
{ |
56697 | 158 |
close_input() |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
159 |
system_output("Terminating Isabelle process") |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
160 |
terminate_process() |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
161 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
162 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
163 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
164 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
165 |
/** stream actors **/ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
166 |
|
46773 | 167 |
/* physical output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
168 |
|
56697 | 169 |
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
|
170 |
{ |
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
|
171 |
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
|
172 |
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
|
173 |
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
|
174 |
|
56697 | 175 |
Simple_Thread.fork(name) { |
46769 | 176 |
try { |
177 |
var result = new StringBuilder(100) |
|
178 |
var finished = false |
|
179 |
while (!finished) { |
|
28045 | 180 |
//{{{ |
181 |
var c = -1 |
|
182 |
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
|
183 |
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
|
184 |
c = reader.read |
28045 | 185 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
186 |
else done = true |
|
187 |
} |
|
188 |
if (result.length > 0) { |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
189 |
output(markup, Nil, List(XML.Text(decode(result.toString)))) |
28045 | 190 |
result.length = 0 |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
191 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
192 |
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
|
193 |
reader.close |
28045 | 194 |
finished = true |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
195 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
196 |
//}}} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
197 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
198 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
199 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
200 |
system_output(name + " terminated") |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
201 |
} |
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
|
202 |
} |
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 |
/* command input */ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
206 |
|
39572 | 207 |
private def input_actor(raw_stream: OutputStream): (Thread, Actor) = |
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
|
208 |
{ |
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
|
209 |
val name = "command_input" |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
210 |
Simple_Thread.actor(name) { |
46769 | 211 |
try { |
212 |
val stream = new BufferedOutputStream(raw_stream) |
|
213 |
var finished = false |
|
214 |
while (!finished) { |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
215 |
//{{{ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
216 |
receive { |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
217 |
case Input_Chunks(chunks) => |
54440 | 218 |
Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream) |
219 |
chunks.foreach(_.write(stream)) |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
220 |
stream.flush |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
221 |
case Close => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
222 |
stream.close |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
223 |
finished = true |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
224 |
case bad => System.err.println(name + ": ignoring bad message " + bad) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
225 |
} |
28045 | 226 |
//}}} |
27963 | 227 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
228 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
229 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
230 |
system_output(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
231 |
} |
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
|
232 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
233 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
234 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
235 |
/* message output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
236 |
|
56697 | 237 |
private def message_output(stream: InputStream): Thread = |
39526 | 238 |
{ |
239 |
class EOF extends Exception |
|
240 |
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
|
241 |
|
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
|
242 |
val name = "message_output" |
56697 | 243 |
Simple_Thread.fork(name) { |
34100 | 244 |
val default_buffer = new Array[Byte](65536) |
245 |
var c = -1 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
246 |
|
52799 | 247 |
def read_int(): Int = |
248 |
//{{{ |
|
34100 | 249 |
{ |
250 |
var n = 0 |
|
251 |
c = stream.read |
|
39526 | 252 |
if (c == -1) throw new EOF |
34100 | 253 |
while (48 <= c && c <= 57) { |
254 |
n = 10 * n + (c - 48) |
|
255 |
c = stream.read |
|
256 |
} |
|
52799 | 257 |
if (c != 10) |
258 |
throw new Protocol_Error("malformed header: expected integer followed by newline") |
|
259 |
else n |
|
260 |
} |
|
261 |
//}}} |
|
34100 | 262 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
263 |
def read_chunk_bytes(): (Array[Byte], Int) = |
52799 | 264 |
//{{{ |
265 |
{ |
|
266 |
val n = read_int() |
|
34100 | 267 |
val buf = |
268 |
if (n <= default_buffer.size) default_buffer |
|
269 |
else new Array[Byte](n) |
|
270 |
||
271 |
var i = 0 |
|
272 |
var m = 0 |
|
273 |
do { |
|
274 |
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
|
275 |
if (m != -1) i += m |
52799 | 276 |
} |
277 |
while (m != -1 && n > i) |
|
34100 | 278 |
|
52799 | 279 |
if (i != n) |
280 |
throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)") |
|
34100 | 281 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
282 |
(buf, n) |
34100 | 283 |
} |
52799 | 284 |
//}}} |
34100 | 285 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
286 |
def read_chunk(): XML.Body = |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
287 |
{ |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
288 |
val (buf, n) = read_chunk_bytes() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
289 |
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
|
290 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
291 |
|
46769 | 292 |
try { |
293 |
do { |
|
294 |
try { |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
295 |
val header = read_chunk() |
46769 | 296 |
header match { |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49445
diff
changeset
|
297 |
case List(XML.Elem(Markup(name, props), Nil)) => |
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49445
diff
changeset
|
298 |
val kind = name.intern |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
299 |
if (kind == Markup.PROTOCOL) { |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
300 |
val (buf, n) = read_chunk_bytes() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
301 |
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
|
302 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
303 |
else { |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
304 |
val body = read_chunk() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
305 |
output(kind, props, body) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
306 |
} |
46769 | 307 |
case _ => |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
308 |
read_chunk() |
46769 | 309 |
throw new Protocol_Error("bad header: " + header.toString) |
310 |
} |
|
28063 | 311 |
} |
46769 | 312 |
catch { case _: EOF => } |
52799 | 313 |
} |
314 |
while (c != -1) |
|
46769 | 315 |
} |
316 |
catch { |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
317 |
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
|
318 |
case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage) |
46769 | 319 |
} |
34100 | 320 |
stream.close |
321 |
||
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
322 |
system_output(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
323 |
} |
39526 | 324 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
325 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
326 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
327 |
|
56387 | 328 |
/** protocol commands **/ |
329 |
||
330 |
def protocol_command_bytes(name: String, args: Bytes*): Unit = |
|
54440 | 331 |
command_input._2 ! Input_Chunks(Bytes(name) :: args.toList) |
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
|
332 |
|
52582 | 333 |
def protocol_command(name: String, args: String*) |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
334 |
{ |
56385 | 335 |
receiver(new Prover.Input(name, args.toList)) |
56387 | 336 |
protocol_command_bytes(name, args.map(Bytes(_)): _*) |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
337 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
338 |
} |