--- 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)