# HG changeset patch # User wenzelm # Date 1520850643 -3600 # Node ID 74958337214dcb9ef43324f8281eed7ed02165c9 # Parent c8e4ee2b5482b1ddae7ea267e980cb9c2beac7c9 tuned signature -- more generic; diff -r c8e4ee2b5482 -r 74958337214d src/Pure/System/tty_loop.scala --- a/src/Pure/System/tty_loop.scala Mon Mar 12 11:17:59 2018 +0100 +++ b/src/Pure/System/tty_loop.scala Mon Mar 12 11:30:43 2018 +0100 @@ -7,13 +7,10 @@ package isabelle -import java.io.{IOException, BufferedReader, BufferedWriter, InputStreamReader} +import java.io.{IOException, Writer, Reader, InputStreamReader, BufferedReader} -class TTY_Loop( - writer: BufferedWriter, - reader: BufferedReader, - interrupt: Option[() => Unit] = None) +class TTY_Loop(writer: Writer, reader: Reader, interrupt: Option[() => Unit] = None) { private val console_output = Future.thread[Unit]("console_output") { try {