# HG changeset patch
# User wenzelm
# Date 1520681647 -3600
# Node ID bd4c440c8be723b70c520880f92e8fb1307d3fba
# Parent  2d9a265b294ec1e2756d64187a32876ef1c4019b
option for console interaction;

diff -r 2d9a265b294e -r bd4c440c8be7 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Mar 10 11:55:54 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sat Mar 10 12:34:07 2018 +0100
@@ -7,7 +7,8 @@
 package isabelle
 
 
-import java.io.{BufferedInputStream, BufferedOutputStream, IOException}
+import java.io.{BufferedInputStream, BufferedOutputStream, BufferedReader, BufferedWriter,
+  InputStreamReader, OutputStreamWriter, IOException}
 import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
 
 
@@ -131,6 +132,18 @@
           case _: SocketException => false
           case _: SocketTimeoutException => false
         }
+
+      def console()
+      {
+        using(connection())(connection =>
+          {
+            val tty_loop =
+              new TTY_Loop(
+                new BufferedWriter(new OutputStreamWriter(connection.socket.getOutputStream)),
+                new BufferedReader(new InputStreamReader(connection.socket.getInputStream)))
+            tty_loop.join
+          })
+      }
     }
   }
 
@@ -201,6 +214,7 @@
   val isabelle_tool =
     Isabelle_Tool("server", "manage resident Isabelle servers", args =>
     {
+      var console = false
       var operation_list = false
       var name = ""
       var port = 0
@@ -210,12 +224,14 @@
 Usage: isabelle server [OPTIONS]
 
   Options are:
-    -L           list servers
+    -C           console interaction with specified server
+    -L           list servers only
     -n NAME      explicit server name
     -p PORT      explicit server port
 
   Manage resident Isabelle servers.
 """,
+          "C" -> (_ => console = true),
           "L" -> (_ => operation_list = true),
           "n:" -> (arg => name = arg),
           "p:" -> (arg => port = Value.Int.parse(arg)))
@@ -230,6 +246,7 @@
       else {
         val (entry, server) = init(name, port)
         Output.writeln(entry.toString, stdout = true)
+        if (console) entry.console()
         server.foreach(_.join)
       }
     })