# 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 {