# HG changeset patch
# User wenzelm
# Date 1502038292 -7200
# Node ID 6e114edae18b5015988d85b2ddcf782387950616
# Parent  7ed911242266620e1f7a892e95c274c90277c64f
proper check for active server;

diff -r 7ed911242266 -r 6e114edae18b src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun Aug 06 17:42:04 2017 +0200
+++ b/src/Pure/Tools/server.scala	Sun Aug 06 18:51:32 2017 +0200
@@ -7,7 +7,8 @@
 package isabelle
 
 
-import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter}
+import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
+  IOException}
 import java.net.{Socket, ServerSocket, InetAddress}
 
 
@@ -28,12 +29,13 @@
     {
       def print: String =
         "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")"
+
+      def active: Boolean =
+        try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true }
+        catch { case _: IOException => false }
     }
   }
 
-  def list(): List[Data.Entry] =
-    using(SQLite.open_database(Data.database))(list(_))
-
   def list(db: SQLite.Database): List[Data.Entry] =
     if (db.tables.contains(Data.table.name)) {
       db.using_statement(Data.table.select())(stmt =>
@@ -46,7 +48,7 @@
     else Nil
 
   def find(db: SQLite.Database, name: String): Option[Data.Entry] =
-    list(db).find(entry => entry.name == name)
+    list(db).find(entry => entry.name == name && entry.active)
 
   def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) =
   {
@@ -60,6 +62,7 @@
 
             Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
             db.create_table(Data.table)
+            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
             db.using_statement(Data.table.insert())(stmt =>
             {
               stmt.string(1) = entry.name
@@ -116,7 +119,10 @@
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      if (operation_list) list().foreach(entry => Console.println(entry.print))
+      if (operation_list) {
+        for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
+          Console.println(entry.print)
+      }
       else {
         val (entry, thread) = start(name, port)
         Console.println(entry.print)