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