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