equal
deleted
inserted
replaced
43 val i = Fifo_Channel.next_fifo() |
43 val i = Fifo_Channel.next_fifo() |
44 val script = |
44 val script = |
45 "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" + |
45 "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" + |
46 "echo -n \"$FIFO\"\n" + |
46 "echo -n \"$FIFO\"\n" + |
47 "mkfifo -m 600 \"$FIFO\"\n" |
47 "mkfifo -m 600 \"$FIFO\"\n" |
48 val (out, err, rc) = Isabelle_System.bash(script) |
48 val result = Isabelle_System.bash(script) |
49 if (rc == 0) out else error(err.trim) |
49 if (result.rc == 0) result.out else error(result.err) |
50 } |
50 } |
51 |
51 |
52 private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete |
52 private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete |
53 |
53 |
54 private def fifo_input_stream(fifo: String): InputStream = new FileInputStream(fifo) |
54 private def fifo_input_stream(fifo: String): InputStream = new FileInputStream(fifo) |