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@38568
|
12 |
InputStream, OutputStream, BufferedOutputStream, IOException}
|
wenzelm@27949
|
13 |
|
wenzelm@32485
|
14 |
import scala.actors.Actor
|
wenzelm@32485
|
15 |
import Actor._
|
wenzelm@39836
|
16 |
import scala.collection.mutable
|
wenzelm@27949
|
17 |
|
wenzelm@27973
|
18 |
|
wenzelm@32485
|
19 |
object Isabelle_Process
|
wenzelm@32485
|
20 |
{
|
wenzelm@27949
|
21 |
/* results */
|
wenzelm@27949
|
22 |
|
wenzelm@39794
|
23 |
object Kind
|
wenzelm@39794
|
24 |
{
|
wenzelm@39794
|
25 |
val message_markup = Map(
|
wenzelm@37705
|
26 |
('A' : Int) -> Markup.INIT,
|
wenzelm@37705
|
27 |
('B' : Int) -> Markup.STATUS,
|
wenzelm@38492
|
28 |
('C' : Int) -> Markup.REPORT,
|
wenzelm@38492
|
29 |
('D' : Int) -> Markup.WRITELN,
|
wenzelm@38492
|
30 |
('E' : Int) -> Markup.TRACING,
|
wenzelm@38492
|
31 |
('F' : Int) -> Markup.WARNING,
|
wenzelm@39782
|
32 |
('G' : Int) -> Markup.ERROR)
|
wenzelm@27949
|
33 |
}
|
wenzelm@27949
|
34 |
|
wenzelm@37705
|
35 |
class Result(val message: XML.Elem)
|
wenzelm@34106
|
36 |
{
|
wenzelm@38486
|
37 |
def kind = message.markup.name
|
wenzelm@38486
|
38 |
def properties = message.markup.properties
|
wenzelm@37705
|
39 |
def body = message.body
|
wenzelm@37705
|
40 |
|
wenzelm@39794
|
41 |
def is_init = kind == Markup.INIT
|
wenzelm@39794
|
42 |
def is_exit = kind == Markup.EXIT
|
wenzelm@39794
|
43 |
def is_stdout = kind == Markup.STDOUT
|
wenzelm@39794
|
44 |
def is_system = kind == Markup.SYSTEM
|
wenzelm@37705
|
45 |
def is_status = kind == Markup.STATUS
|
wenzelm@38492
|
46 |
def is_report = kind == Markup.REPORT
|
wenzelm@39855
|
47 |
def is_ready = is_status && {
|
wenzelm@39855
|
48 |
body match {
|
wenzelm@39855
|
49 |
case List(XML.Elem(Markup(Markup.READY, _), _)) => true
|
wenzelm@39855
|
50 |
case _ => false
|
wenzelm@39855
|
51 |
}}
|
wenzelm@34106
|
52 |
|
wenzelm@34106
|
53 |
override def toString: String =
|
wenzelm@34106
|
54 |
{
|
wenzelm@29522
|
55 |
val res =
|
wenzelm@38492
|
56 |
if (is_status || is_report) message.body.map(_.toString).mkString
|
wenzelm@37705
|
57 |
else Pretty.string_of(message.body)
|
wenzelm@38486
|
58 |
if (properties.isEmpty)
|
wenzelm@29572
|
59 |
kind.toString + " [[" + res + "]]"
|
wenzelm@29572
|
60 |
else
|
wenzelm@29572
|
61 |
kind.toString + " " +
|
wenzelm@38486
|
62 |
(for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
|
wenzelm@27949
|
63 |
}
|
wenzelm@27973
|
64 |
}
|
wenzelm@27973
|
65 |
}
|
wenzelm@27973
|
66 |
|
wenzelm@27973
|
67 |
|
wenzelm@39797
|
68 |
class Isabelle_Process(system: Isabelle_System, timeout: Int, receiver: Actor, args: String*)
|
wenzelm@29192
|
69 |
{
|
wenzelm@31800
|
70 |
import Isabelle_Process._
|
wenzelm@29194
|
71 |
|
wenzelm@27973
|
72 |
|
wenzelm@29192
|
73 |
/* demo constructor */
|
wenzelm@27973
|
74 |
|
wenzelm@29192
|
75 |
def this(args: String*) =
|
wenzelm@39797
|
76 |
this(new Isabelle_System, 10000,
|
wenzelm@34213
|
77 |
actor { loop { react { case res => Console.println(res) } } }, args: _*)
|
wenzelm@29174
|
78 |
|
wenzelm@29174
|
79 |
|
wenzelm@39837
|
80 |
/* system log */
|
wenzelm@39837
|
81 |
|
wenzelm@39837
|
82 |
private val system_results = new mutable.ListBuffer[String]
|
wenzelm@39837
|
83 |
|
wenzelm@39837
|
84 |
private def system_result(text: String)
|
wenzelm@39837
|
85 |
{
|
wenzelm@39837
|
86 |
synchronized { system_results += text }
|
wenzelm@39837
|
87 |
receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
|
wenzelm@39837
|
88 |
}
|
wenzelm@39837
|
89 |
|
wenzelm@39837
|
90 |
def syslog(): List[String] = synchronized { system_results.toList }
|
wenzelm@39837
|
91 |
|
wenzelm@39837
|
92 |
|
wenzelm@39837
|
93 |
/* results */
|
wenzelm@39837
|
94 |
|
wenzelm@39837
|
95 |
private val xml_cache = new XML.Cache(131071)
|
wenzelm@39837
|
96 |
|
wenzelm@39837
|
97 |
private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
|
wenzelm@39837
|
98 |
{
|
wenzelm@39849
|
99 |
if (kind == Markup.INIT) rm_fifos()
|
wenzelm@39837
|
100 |
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
|
wenzelm@39837
|
101 |
xml_cache.cache_tree(msg)((message: XML.Tree) =>
|
wenzelm@39837
|
102 |
receiver ! new Result(message.asInstanceOf[XML.Elem]))
|
wenzelm@39837
|
103 |
}
|
wenzelm@39837
|
104 |
|
wenzelm@39837
|
105 |
private def put_result(kind: String, text: String)
|
wenzelm@39837
|
106 |
{
|
wenzelm@39837
|
107 |
put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
|
wenzelm@39837
|
108 |
}
|
wenzelm@39837
|
109 |
|
wenzelm@39837
|
110 |
|
wenzelm@39797
|
111 |
/* input actors */
|
wenzelm@27973
|
112 |
|
wenzelm@39797
|
113 |
private case class Input_Text(text: String)
|
wenzelm@39797
|
114 |
private case class Input_Chunks(chunks: List[Array[Byte]])
|
wenzelm@39797
|
115 |
|
wenzelm@39797
|
116 |
private case object Close
|
wenzelm@39849
|
117 |
private def close(p: (Thread, Actor))
|
wenzelm@39849
|
118 |
{
|
wenzelm@39849
|
119 |
if (p != null && p._1.isAlive) {
|
wenzelm@39849
|
120 |
p._2 ! Close
|
wenzelm@39849
|
121 |
p._1.join
|
wenzelm@39849
|
122 |
}
|
wenzelm@39849
|
123 |
}
|
wenzelm@39797
|
124 |
|
wenzelm@39849
|
125 |
@volatile private var standard_input: (Thread, Actor) = null
|
wenzelm@39849
|
126 |
@volatile private var command_input: (Thread, Actor) = null
|
wenzelm@39797
|
127 |
|
wenzelm@39797
|
128 |
|
wenzelm@39849
|
129 |
/** process manager **/
|
wenzelm@39797
|
130 |
|
wenzelm@39797
|
131 |
private val in_fifo = system.mk_fifo()
|
wenzelm@39797
|
132 |
private val out_fifo = system.mk_fifo()
|
wenzelm@39797
|
133 |
private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
|
wenzelm@39797
|
134 |
|
wenzelm@39849
|
135 |
private val process =
|
wenzelm@39797
|
136 |
try {
|
wenzelm@39797
|
137 |
val cmdline =
|
wenzelm@39797
|
138 |
List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
|
wenzelm@39849
|
139 |
new system.Managed_Process(true, cmdline: _*)
|
wenzelm@39797
|
140 |
}
|
wenzelm@39797
|
141 |
catch { case e: IOException => rm_fifos(); throw(e) }
|
wenzelm@39797
|
142 |
|
wenzelm@39851
|
143 |
val process_result =
|
wenzelm@39851
|
144 |
Simple_Thread.future("process_result") { process.join }
|
wenzelm@39851
|
145 |
|
wenzelm@39849
|
146 |
private def terminate_process()
|
wenzelm@39849
|
147 |
{
|
wenzelm@39849
|
148 |
try { process.terminate }
|
wenzelm@39849
|
149 |
catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
|
wenzelm@39849
|
150 |
}
|
wenzelm@39797
|
151 |
|
wenzelm@39849
|
152 |
private val process_manager = Simple_Thread.fork("process_manager")
|
wenzelm@39836
|
153 |
{
|
wenzelm@39797
|
154 |
val (startup_failed, startup_output) =
|
wenzelm@39797
|
155 |
{
|
wenzelm@39797
|
156 |
val expired = System.currentTimeMillis() + timeout
|
wenzelm@39797
|
157 |
val result = new StringBuilder(100)
|
wenzelm@39797
|
158 |
|
wenzelm@39851
|
159 |
var finished: Option[Boolean] = None
|
wenzelm@39851
|
160 |
while (finished.isEmpty && System.currentTimeMillis() <= expired) {
|
wenzelm@39851
|
161 |
while (finished.isEmpty && process.stdout.ready) {
|
wenzelm@39849
|
162 |
val c = process.stdout.read
|
wenzelm@39851
|
163 |
if (c == 2) finished = Some(true)
|
wenzelm@39797
|
164 |
else result += c.toChar
|
wenzelm@39797
|
165 |
}
|
wenzelm@39851
|
166 |
if (process_result.is_finished) finished = Some(false)
|
wenzelm@39851
|
167 |
else Thread.sleep(10)
|
wenzelm@39797
|
168 |
}
|
wenzelm@39913
|
169 |
(finished.isEmpty || !finished.get, result.toString.trim)
|
wenzelm@39797
|
170 |
}
|
wenzelm@39836
|
171 |
system_result(startup_output)
|
wenzelm@39836
|
172 |
|
wenzelm@39797
|
173 |
if (startup_failed) {
|
wenzelm@39797
|
174 |
put_result(Markup.EXIT, "127")
|
wenzelm@39849
|
175 |
process.stdin.close
|
wenzelm@39849
|
176 |
Thread.sleep(300)
|
wenzelm@39849
|
177 |
terminate_process()
|
wenzelm@39851
|
178 |
process_result.join
|
wenzelm@39797
|
179 |
}
|
wenzelm@39797
|
180 |
else {
|
wenzelm@39799
|
181 |
// rendezvous
|
wenzelm@39799
|
182 |
val command_stream = system.fifo_output_stream(in_fifo)
|
wenzelm@39799
|
183 |
val message_stream = system.fifo_input_stream(out_fifo)
|
wenzelm@39799
|
184 |
|
wenzelm@39849
|
185 |
standard_input = stdin_actor()
|
wenzelm@39836
|
186 |
val stdout = stdout_actor()
|
wenzelm@39849
|
187 |
command_input = input_actor(command_stream)
|
wenzelm@39836
|
188 |
val message = message_actor(message_stream)
|
wenzelm@39797
|
189 |
|
wenzelm@39851
|
190 |
val rc = process_result.join
|
wenzelm@39908
|
191 |
system_result("process terminated")
|
wenzelm@39849
|
192 |
for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
|
wenzelm@39836
|
193 |
system_result("process_manager terminated")
|
wenzelm@39797
|
194 |
put_result(Markup.EXIT, rc.toString)
|
wenzelm@39797
|
195 |
}
|
wenzelm@39797
|
196 |
rm_fifos()
|
wenzelm@39797
|
197 |
}
|
wenzelm@27973
|
198 |
|
wenzelm@39849
|
199 |
|
wenzelm@39849
|
200 |
/* management methods */
|
wenzelm@39849
|
201 |
|
wenzelm@39836
|
202 |
def join() { process_manager.join() }
|
wenzelm@27973
|
203 |
|
wenzelm@38568
|
204 |
def interrupt()
|
wenzelm@38568
|
205 |
{
|
wenzelm@39849
|
206 |
try { process.interrupt }
|
wenzelm@39849
|
207 |
catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
|
wenzelm@38568
|
208 |
}
|
wenzelm@38568
|
209 |
|
wenzelm@39849
|
210 |
def terminate()
|
wenzelm@38568
|
211 |
{
|
wenzelm@39849
|
212 |
close()
|
wenzelm@39849
|
213 |
system_result("Terminating Isabelle process")
|
wenzelm@39849
|
214 |
terminate_process()
|
wenzelm@27973
|
215 |
}
|
wenzelm@27973
|
216 |
|
wenzelm@27949
|
217 |
|
wenzelm@27949
|
218 |
|
wenzelm@38557
|
219 |
/** stream actors **/
|
wenzelm@27949
|
220 |
|
wenzelm@38568
|
221 |
/* raw stdin */
|
wenzelm@38568
|
222 |
|
wenzelm@39836
|
223 |
private def stdin_actor(): (Thread, Actor) =
|
wenzelm@39797
|
224 |
{
|
wenzelm@39797
|
225 |
val name = "standard_input"
|
wenzelm@38895
|
226 |
Simple_Thread.actor(name) {
|
wenzelm@27949
|
227 |
var finished = false
|
wenzelm@27949
|
228 |
while (!finished) {
|
wenzelm@27949
|
229 |
try {
|
wenzelm@27949
|
230 |
//{{{
|
wenzelm@38557
|
231 |
receive {
|
wenzelm@38568
|
232 |
case Input_Text(text) =>
|
wenzelm@39849
|
233 |
process.stdin.write(text)
|
wenzelm@39849
|
234 |
process.stdin.flush
|
wenzelm@38557
|
235 |
case Close =>
|
wenzelm@39849
|
236 |
process.stdin.close
|
wenzelm@38557
|
237 |
finished = true
|
wenzelm@38557
|
238 |
case bad => System.err.println(name + ": ignoring bad message " + bad)
|
wenzelm@27949
|
239 |
}
|
wenzelm@27949
|
240 |
//}}}
|
wenzelm@27949
|
241 |
}
|
wenzelm@39794
|
242 |
catch { case e: IOException => system_result(name + ": " + e.getMessage) }
|
wenzelm@27949
|
243 |
}
|
wenzelm@39794
|
244 |
system_result(name + " terminated")
|
wenzelm@27949
|
245 |
}
|
wenzelm@39797
|
246 |
}
|
wenzelm@27949
|
247 |
|
wenzelm@27949
|
248 |
|
wenzelm@38568
|
249 |
/* raw stdout */
|
wenzelm@27949
|
250 |
|
wenzelm@39836
|
251 |
private def stdout_actor(): (Thread, Actor) =
|
wenzelm@39797
|
252 |
{
|
wenzelm@39797
|
253 |
val name = "standard_output"
|
wenzelm@38895
|
254 |
Simple_Thread.actor(name) {
|
wenzelm@27949
|
255 |
var result = new StringBuilder(100)
|
wenzelm@27949
|
256 |
|
wenzelm@27949
|
257 |
var finished = false
|
wenzelm@27949
|
258 |
while (!finished) {
|
wenzelm@27949
|
259 |
try {
|
wenzelm@27949
|
260 |
//{{{
|
wenzelm@27949
|
261 |
var c = -1
|
wenzelm@27949
|
262 |
var done = false
|
wenzelm@39849
|
263 |
while (!done && (result.length == 0 || process.stdout.ready)) {
|
wenzelm@39849
|
264 |
c = process.stdout.read
|
wenzelm@28045
|
265 |
if (c >= 0) result.append(c.asInstanceOf[Char])
|
wenzelm@27949
|
266 |
else done = true
|
wenzelm@27949
|
267 |
}
|
wenzelm@27949
|
268 |
if (result.length > 0) {
|
wenzelm@38568
|
269 |
put_result(Markup.STDOUT, result.toString)
|
wenzelm@27949
|
270 |
result.length = 0
|
wenzelm@27949
|
271 |
}
|
wenzelm@27949
|
272 |
else {
|
wenzelm@39849
|
273 |
process.stdout.close
|
wenzelm@27949
|
274 |
finished = true
|
wenzelm@38568
|
275 |
}
|
wenzelm@38568
|
276 |
//}}}
|
wenzelm@38568
|
277 |
}
|
wenzelm@39794
|
278 |
catch { case e: IOException => system_result(name + ": " + e.getMessage) }
|
wenzelm@38568
|
279 |
}
|
wenzelm@39794
|
280 |
system_result(name + " terminated")
|
wenzelm@38568
|
281 |
}
|
wenzelm@39797
|
282 |
}
|
wenzelm@38568
|
283 |
|
wenzelm@38568
|
284 |
|
wenzelm@38568
|
285 |
/* command input */
|
wenzelm@38568
|
286 |
|
wenzelm@39836
|
287 |
private def input_actor(raw_stream: OutputStream): (Thread, Actor) =
|
wenzelm@39797
|
288 |
{
|
wenzelm@39797
|
289 |
val name = "command_input"
|
wenzelm@38895
|
290 |
Simple_Thread.actor(name) {
|
wenzelm@39799
|
291 |
val stream = new BufferedOutputStream(raw_stream)
|
wenzelm@38568
|
292 |
var finished = false
|
wenzelm@38568
|
293 |
while (!finished) {
|
wenzelm@38568
|
294 |
try {
|
wenzelm@38568
|
295 |
//{{{
|
wenzelm@38568
|
296 |
receive {
|
wenzelm@38568
|
297 |
case Input_Chunks(chunks) =>
|
wenzelm@38568
|
298 |
stream.write(Standard_System.string_bytes(
|
wenzelm@38568
|
299 |
chunks.map(_.length).mkString("", ",", "\n")));
|
wenzelm@38568
|
300 |
chunks.foreach(stream.write(_));
|
wenzelm@38568
|
301 |
stream.flush
|
wenzelm@38568
|
302 |
case Close =>
|
wenzelm@38568
|
303 |
stream.close
|
wenzelm@38568
|
304 |
finished = true
|
wenzelm@38568
|
305 |
case bad => System.err.println(name + ": ignoring bad message " + bad)
|
wenzelm@27949
|
306 |
}
|
wenzelm@27949
|
307 |
//}}}
|
wenzelm@27963
|
308 |
}
|
wenzelm@39794
|
309 |
catch { case e: IOException => system_result(name + ": " + e.getMessage) }
|
wenzelm@27949
|
310 |
}
|
wenzelm@39794
|
311 |
system_result(name + " terminated")
|
wenzelm@27949
|
312 |
}
|
wenzelm@39797
|
313 |
}
|
wenzelm@27949
|
314 |
|
wenzelm@27949
|
315 |
|
wenzelm@38557
|
316 |
/* message output */
|
wenzelm@27949
|
317 |
|
wenzelm@39836
|
318 |
private def message_actor(stream: InputStream): (Thread, Actor) =
|
wenzelm@39795
|
319 |
{
|
wenzelm@39795
|
320 |
class EOF extends Exception
|
wenzelm@39795
|
321 |
class Protocol_Error(msg: String) extends Exception(msg)
|
wenzelm@38557
|
322 |
|
wenzelm@39797
|
323 |
val name = "message_output"
|
wenzelm@38895
|
324 |
Simple_Thread.actor(name) {
|
wenzelm@34106
|
325 |
val default_buffer = new Array[Byte](65536)
|
wenzelm@34106
|
326 |
var c = -1
|
wenzelm@28045
|
327 |
|
wenzelm@38867
|
328 |
def read_chunk(): XML.Body =
|
wenzelm@34106
|
329 |
{
|
wenzelm@34106
|
330 |
//{{{
|
wenzelm@34106
|
331 |
// chunk size
|
wenzelm@34106
|
332 |
var n = 0
|
wenzelm@34106
|
333 |
c = stream.read
|
wenzelm@39795
|
334 |
if (c == -1) throw new EOF
|
wenzelm@34106
|
335 |
while (48 <= c && c <= 57) {
|
wenzelm@34106
|
336 |
n = 10 * n + (c - 48)
|
wenzelm@34106
|
337 |
c = stream.read
|
wenzelm@34106
|
338 |
}
|
wenzelm@34106
|
339 |
if (c != 10) throw new Protocol_Error("bad message chunk header")
|
wenzelm@34106
|
340 |
|
wenzelm@34106
|
341 |
// chunk content
|
wenzelm@34106
|
342 |
val buf =
|
wenzelm@34106
|
343 |
if (n <= default_buffer.size) default_buffer
|
wenzelm@34106
|
344 |
else new Array[Byte](n)
|
wenzelm@34106
|
345 |
|
wenzelm@34106
|
346 |
var i = 0
|
wenzelm@34106
|
347 |
var m = 0
|
wenzelm@34106
|
348 |
do {
|
wenzelm@34106
|
349 |
m = stream.read(buf, i, n - i)
|
wenzelm@34106
|
350 |
i += m
|
wenzelm@34106
|
351 |
} while (m > 0 && n > i)
|
wenzelm@34106
|
352 |
|
wenzelm@34106
|
353 |
if (i != n) throw new Protocol_Error("bad message chunk content")
|
wenzelm@34106
|
354 |
|
wenzelm@34106
|
355 |
YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
|
wenzelm@34106
|
356 |
//}}}
|
wenzelm@34106
|
357 |
}
|
wenzelm@34106
|
358 |
|
wenzelm@34106
|
359 |
do {
|
wenzelm@28045
|
360 |
try {
|
wenzelm@38691
|
361 |
val header = read_chunk()
|
wenzelm@38691
|
362 |
val body = read_chunk()
|
wenzelm@38691
|
363 |
header match {
|
wenzelm@38691
|
364 |
case List(XML.Elem(Markup(name, props), Nil))
|
wenzelm@39794
|
365 |
if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
|
wenzelm@39794
|
366 |
put_result(Kind.message_markup(name(0)), props, body)
|
wenzelm@38691
|
367 |
case _ => throw new Protocol_Error("bad header: " + header.toString)
|
wenzelm@34106
|
368 |
}
|
wenzelm@28045
|
369 |
}
|
wenzelm@28063
|
370 |
catch {
|
wenzelm@39794
|
371 |
case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
|
wenzelm@39794
|
372 |
case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
|
wenzelm@39795
|
373 |
case _: EOF =>
|
wenzelm@28063
|
374 |
}
|
wenzelm@34106
|
375 |
} while (c != -1)
|
wenzelm@34106
|
376 |
stream.close
|
wenzelm@34106
|
377 |
|
wenzelm@39794
|
378 |
system_result(name + " terminated")
|
wenzelm@38557
|
379 |
}
|
wenzelm@39795
|
380 |
}
|
wenzelm@38557
|
381 |
|
wenzelm@38557
|
382 |
|
wenzelm@38557
|
383 |
/** main methods **/
|
wenzelm@38557
|
384 |
|
wenzelm@39849
|
385 |
def input_raw(text: String): Unit = standard_input._2 ! Input_Text(text)
|
wenzelm@38557
|
386 |
|
wenzelm@38654
|
387 |
def input_bytes(name: String, args: Array[Byte]*): Unit =
|
wenzelm@39849
|
388 |
command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
|
wenzelm@38654
|
389 |
|
wenzelm@38568
|
390 |
def input(name: String, args: String*): Unit =
|
wenzelm@38654
|
391 |
input_bytes(name, args.map(Standard_System.string_bytes): _*)
|
wenzelm@38557
|
392 |
|
wenzelm@39797
|
393 |
def close(): Unit = { close(command_input); close(standard_input) }
|
wenzelm@27949
|
394 |
}
|