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