# HG changeset patch
# User wenzelm
# Date 1502018978 -7200
# Node ID a426e826e84cf8d086f0609932e331a5c5b1b9b3
# Parent  23eaab37e4a844193d083482bf270d2601bc3a33
more options;
misc tuning and clarification;

diff -r 23eaab37e4a8 -r a426e826e84c src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Aug 05 20:08:41 2017 +0200
+++ b/src/Pure/Tools/server.scala	Sun Aug 06 13:29:38 2017 +0200
@@ -26,7 +26,9 @@
 
     sealed case class Entry(server_name: String, server_port: Int, password: String)
     {
-      def address: String = "127.0.0.1:" + server_port
+      def print: String =
+        "server " + quote(server_name) + " = 127.0.0.1:" + server_port +
+        " (password " + quote(password) + ")"
     }
   }
 
@@ -47,15 +49,14 @@
   def find(db: SQLite.Database, name: String): Option[Data.Entry] =
     list(db).find(entry => entry.server_name == name)
 
-  def start(name: String = "", port: Int = 0): (Data.Entry, Boolean) =
+  def start(name: String = "", port: Int = 0, password: String = ""): (Data.Entry, Option[Thread]) =
   {
     using(SQLite.open_database(Data.database))(db =>
       db.transaction {
         find(db, name) match {
-          case Some(entry) => (entry, false)
+          case Some(entry) => (entry, None)
           case None =>
-            val socket = new ServerSocket(port, 50, InetAddress.getByName("127.0.0.1"))
-            val server = new Server(socket)
+            val server = new Server(port, password)
             val entry = Data.Entry(name, server.port, server.password)
 
             Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
@@ -67,7 +68,8 @@
               stmt.string(3) = entry.password
               stmt.execute()
             })
-            (entry, true)
+
+            (entry, Some(server.thread))
         }
       })
   }
@@ -93,30 +95,42 @@
   val isabelle_tool =
     Isabelle_Tool("server", "manage resident Isabelle servers", args =>
     {
-      var list_servers = false
+      var operation_list = false
+      var name = ""
+      var port = 0
 
       val getopts =
         Getopts("""
 Usage: isabelle server [OPTIONS]
 
   Options are:
-    -l           list servers
+    -L           list servers
+    -n NAME      explicit server name
+    -p PORT      explicit server port
 
   Manage resident Isabelle servers.
 """,
-          "l" -> (_ => list_servers = true))
+          "L" -> (_ => operation_list = true),
+          "n:" -> (arg => name = arg),
+          "p:" -> (arg => port = Value.Int.parse(arg)))
 
       val more_args = getopts(args)
-      if (more_args.nonEmpty || !list_servers) getopts.usage()
+      if (more_args.nonEmpty) getopts.usage()
 
-      if (list_servers) list().foreach(entry =>
-        Console.println("server " + quote(entry.server_name) + " = " + entry.address +
-          " (password " + quote(entry.password) + ")"))
+      if (operation_list) list().foreach(entry => Console.println(entry.print))
+      else {
+        val (entry, thread) = start(name, port)
+        Console.println(entry.print)
+        thread.foreach(_.join)
+      }
     })
 }
 
-class Server private(val socket: ServerSocket)
+class Server private(_port: Int, _password: String)
 {
+  val socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
   def port: Int = socket.getLocalPort
-  val password = UUID.randomUUID().toString
+  val password: String = proper_string(_password) getOrElse UUID.randomUUID().toString
+
+  lazy val thread: Thread = Thread.currentThread // FIXME
 }