# HG changeset patch
# User wenzelm
# Date 1520687518 -3600
# Node ID 33199d03350567cef6ef65898ddf088feab32e0d
# Parent  8ebae6708590782822481acd36e8e2601f824ba2
more options: client without implicit server startup;

diff -r 8ebae6708590 -r 33199d033505 lib/Tools/client
--- a/lib/Tools/client	Sat Mar 10 13:54:55 2018 +0100
+++ b/lib/Tools/client	Sat Mar 10 14:11:58 2018 +0100
@@ -62,8 +62,8 @@
 
 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
 then
-  exec "$ISABELLE_LINE_EDITOR" isabelle server -C "${SERVER_OPTS[@]}"
+  exec "$ISABELLE_LINE_EDITOR" isabelle server -s -C "${SERVER_OPTS[@]}"
 else
   echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
-  exec isabelle server -C "${SERVER_OPTS[@]}"
+  exec isabelle server -s -C "${SERVER_OPTS[@]}"
 fi
diff -r 8ebae6708590 -r 33199d033505 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Mar 10 13:54:55 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sat Mar 10 14:11:58 2018 +0100
@@ -183,7 +183,8 @@
   def find(db: SQLite.Database, name: String): Option[Info] =
     list(db).find(server_info => server_info.name == name && server_info.active)
 
-  def init(name: String = "", port: Int = 0): (Info, Option[Server]) =
+  def init(name: String = "", port: Int = 0, existing_server: Boolean = false)
+    : (Info, Option[Server]) =
   {
     using(SQLite.open_database(Data.database))(db =>
       {
@@ -198,6 +199,11 @@
           find(db, name) match {
             case Some(server_info) => (server_info, None)
             case None =>
+              if (existing_server) {
+                if (name == "") error("Isabelle server not running")
+                else error("Isabelle server " + quote(name) + " not running")
+              }
+
               val server = new Server(port)
               val server_info = Info(name, server.port, server.password)
 
@@ -241,6 +247,7 @@
       var operation_list = false
       var name = ""
       var port = 0
+      var existing_server = false
 
       val getopts =
         Getopts("""
@@ -251,13 +258,15 @@
     -L           list servers only
     -n NAME      explicit server name
     -p PORT      explicit server port
+    -s           assume existing server, no implicit startup
 
   Manage resident Isabelle servers.
 """,
           "C" -> (_ => console = true),
           "L" -> (_ => operation_list = true),
           "n:" -> (arg => name = arg),
-          "p:" -> (arg => port = Value.Int.parse(arg)))
+          "p:" -> (arg => port = Value.Int.parse(arg)),
+          "s" -> (_ => existing_server = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
@@ -269,7 +278,7 @@
         } Output.writeln(server_info.toString, stdout = true)
       }
       else {
-        val (server_info, server) = init(name, port)
+        val (server_info, server) = init(name, port = port, existing_server = existing_server)
         Output.writeln(server_info.toString, stdout = true)
         if (console) server_info.console()
         server.foreach(_.join)