# HG changeset patch
# User wenzelm
# Date 1520848502 -3600
# Node ID e135d03f656f1837ccb18827a983ce28cfcfddf2
# Parent  069aa924671fee8c03bdd557e2f44e34c62b6fe9
tuned signature;

diff -r 069aa924671f -r e135d03f656f src/Pure/System/tty_loop.scala
--- a/src/Pure/System/tty_loop.scala	Mon Mar 12 10:50:26 2018 +0100
+++ b/src/Pure/System/tty_loop.scala	Mon Mar 12 10:55:02 2018 +0100
@@ -11,9 +11,9 @@
 
 
 class TTY_Loop(
-  process_writer: BufferedWriter,
-  process_reader: BufferedReader,
-  process_interrupt: Option[() => Unit] = None)
+  writer: BufferedWriter,
+  reader: BufferedReader,
+  interrupt: Option[() => Unit] = None)
 {
   private val console_output = Future.thread[Unit]("console_output") {
     try {
@@ -22,8 +22,8 @@
       while (!finished) {
         var c = -1
         var done = false
-        while (!done && (result.length == 0 || process_reader.ready)) {
-          c = process_reader.read
+        while (!done && (result.length == 0 || reader.ready)) {
+          c = reader.read
           if (c >= 0) result.append(c.asInstanceOf[Char])
           else done = true
         }
@@ -33,7 +33,7 @@
           result.length = 0
         }
         else {
-          process_reader.close()
+          reader.close()
           finished = true
         }
       }
@@ -50,21 +50,20 @@
         while (!finished) {
           console_reader.readLine() match {
             case null =>
-              process_writer.close()
+              writer.close()
               finished = true
             case line =>
-              process_writer.write(line)
-              process_writer.write("\n")
-              process_writer.flush()
+              writer.write(line)
+              writer.write("\n")
+              writer.flush()
           }
         }
       }
       catch { case e: IOException => case Exn.Interrupt() => }
     }
-    process_interrupt match {
+    interrupt match {
       case None => body
-      case Some(interrupt) =>
-        POSIX_Interrupt.handler { interrupt() } { body }
+      case Some(int) => POSIX_Interrupt.handler { int() } { body }
     }
   }
 
diff -r 069aa924671f -r e135d03f656f src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Mon Mar 12 10:50:26 2018 +0100
+++ b/src/Pure/Tools/server.scala	Mon Mar 12 10:55:02 2018 +0100
@@ -109,11 +109,11 @@
 
     def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) }
 
-    def tty_loop(process_interrupt: Option[() => Unit] = None): TTY_Loop =
+    def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
       new TTY_Loop(
         new BufferedWriter(new OutputStreamWriter(socket.getOutputStream)),
         new BufferedReader(new InputStreamReader(socket.getInputStream)),
-        process_interrupt = process_interrupt)
+        interrupt = interrupt)
 
     private val in = new BufferedInputStream(socket.getInputStream)
     private val out = new BufferedOutputStream(socket.getOutputStream)
@@ -185,10 +185,9 @@
         case _: SocketTimeoutException => false
       }
 
-    def console(process_interrupt: Option[() => Unit] = None)
+    def console(interrupt: Option[() => Unit] = None)
     {
-      using(connection())(connection =>
-        connection.tty_loop(process_interrupt = process_interrupt).join)
+      using(connection())(connection => connection.tty_loop(interrupt = interrupt).join)
     }
   }