# HG changeset patch
# User wenzelm
# Date 1520604395 -3600
# Node ID 1cfc7541012e1a1c485c2090ac7e3e32bf0b1269
# Parent  bb2bbabf3d37724987ba508328c557d327640299
Entry.connection: proview password here;
more robust checks;

diff -r bb2bbabf3d37 -r 1cfc7541012e src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 09 14:35:18 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 15:06:35 2018 +0100
@@ -9,7 +9,7 @@
 
 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
   IOException}
-import java.net.{Socket, SocketException, ServerSocket, InetAddress}
+import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
 
 
 object Server
@@ -65,7 +65,7 @@
       require(split_lines(msg).length <= 1)
       writer.write(msg)
       writer.newLine()
-      writer.flush()
+      try { writer.flush() } catch { case _: SocketException => }
     }
 
     def reply(r: Server.Reply.Value, t: JSON.T)
@@ -100,11 +100,25 @@
         "server " + quote(name) + " = " + print(port, password)
 
       def connection(): Connection =
-        Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
+      {
+        val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
+        connection.write_line(password)
+        connection
+      }
 
       def active(): Boolean =
-        try { connection().close; true }
-        catch { case _: IOException => false }
+        try {
+          using(connection())(connection =>
+            {
+              connection.socket.setSoTimeout(500)
+              connection.read_line() == Some(Reply.OK.toString)
+            })
+        }
+        catch {
+          case _: IOException => false
+          case _: SocketException => false
+          case _: SocketTimeoutException => false
+        }
     }
   }
 
@@ -155,12 +169,8 @@
       db.transaction {
         find(db, name) match {
           case Some(entry) =>
-            using(entry.connection())(connection =>
-              {
-                connection.write_line(entry.password)
-                connection.write_line("shutdown")
-              })
-            while(entry.active) { Thread.sleep(100) }
+            using(entry.connection())(_.write_line("shutdown"))
+            while(entry.active) { Thread.sleep(50) }
             true
           case None => false
         }