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