67802
|
1 |
/* Title: Pure/System/tty_loop.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Line-oriented TTY loop.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
import java.io.{IOException, BufferedReader, BufferedWriter, InputStreamReader}
|
|
11 |
|
|
12 |
|
|
13 |
class TTY_Loop(
|
|
14 |
process_writer: BufferedWriter,
|
|
15 |
process_reader: BufferedReader,
|
|
16 |
process_interrupt: () => Unit = () => ())
|
|
17 |
{
|
|
18 |
private val console_output = Future.thread[Unit]("console_output") {
|
|
19 |
try {
|
|
20 |
var result = new StringBuilder(100)
|
|
21 |
var finished = false
|
|
22 |
while (!finished) {
|
|
23 |
var c = -1
|
|
24 |
var done = false
|
|
25 |
while (!done && (result.length == 0 || process_reader.ready)) {
|
|
26 |
c = process_reader.read
|
|
27 |
if (c >= 0) result.append(c.asInstanceOf[Char])
|
|
28 |
else done = true
|
|
29 |
}
|
|
30 |
if (result.length > 0) {
|
|
31 |
System.out.print(result.toString)
|
|
32 |
System.out.flush()
|
|
33 |
result.length = 0
|
|
34 |
}
|
|
35 |
else {
|
|
36 |
process_reader.close()
|
|
37 |
finished = true
|
|
38 |
}
|
|
39 |
}
|
|
40 |
}
|
|
41 |
catch { case e: IOException => case Exn.Interrupt() => }
|
|
42 |
}
|
|
43 |
|
|
44 |
private val console_input = Future.thread[Unit]("console_input") {
|
|
45 |
val console_reader = new BufferedReader(new InputStreamReader(System.in))
|
|
46 |
POSIX_Interrupt.handler { process_interrupt() } {
|
|
47 |
try {
|
|
48 |
var finished = false
|
|
49 |
while (!finished) {
|
|
50 |
console_reader.readLine() match {
|
|
51 |
case null =>
|
|
52 |
process_writer.close()
|
|
53 |
finished = true
|
|
54 |
case line =>
|
|
55 |
process_writer.write(line)
|
|
56 |
process_writer.write("\n")
|
|
57 |
process_writer.flush()
|
|
58 |
}
|
|
59 |
}
|
|
60 |
}
|
|
61 |
catch { case e: IOException => case Exn.Interrupt() => }
|
|
62 |
}
|
|
63 |
}
|
|
64 |
|
|
65 |
def join { console_output.join; console_input.join }
|
|
66 |
|
|
67 |
def cancel { console_input.cancel }
|
|
68 |
}
|