# HG changeset patch
# User wenzelm
# Date 1520850699 -3600
# Node ID 932d01332c6c78338458cfc80460f07e964e1acd
# Parent  74958337214dcb9ef43324f8281eed7ed02165c9
re-use existing in/out streams;

diff -r 74958337214d -r 932d01332c6c src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Mon Mar 12 11:30:43 2018 +0100
+++ b/src/Pure/Tools/server.scala	Mon Mar 12 11:31:39 2018 +0100
@@ -19,8 +19,8 @@
 package isabelle
 
 
-import java.io.{BufferedInputStream, BufferedOutputStream, BufferedReader, BufferedWriter,
-  InputStreamReader, OutputStreamWriter, IOException}
+import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter,
+  IOException}
 import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
 
 
@@ -109,15 +109,12 @@
 
     def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) }
 
-    def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
-      new TTY_Loop(
-        new BufferedWriter(new OutputStreamWriter(socket.getOutputStream)),
-        new BufferedReader(new InputStreamReader(socket.getInputStream)),
-        interrupt = interrupt)
-
     private val in = new BufferedInputStream(socket.getInputStream)
     private val out = new BufferedOutputStream(socket.getOutputStream)
 
+    def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
+      new TTY_Loop(new OutputStreamWriter(out), new InputStreamReader(in), interrupt = interrupt)
+
     def read_message(): Option[String] =
       try {
         Bytes.read_line(in).map(_.text) match {