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