# HG changeset patch
# User wenzelm
# Date 1520778080 -3600
# Node ID 0e2484df2491c21c20126f8a5d0714d151a4519d
# Parent  82fb12061069973a12bd1aa1dd8fde4e311585f4
clarified default server name;

diff -r 82fb12061069 -r 0e2484df2491 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun Mar 11 15:15:30 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sun Mar 11 15:21:20 2018 +0100
@@ -193,6 +193,8 @@
 
   /* per-user servers */
 
+  val default_name = "isabelle"
+
   def print(port: Int, password: String): String =
     "127.0.0.1:" + port + " (password " + quote(password) + ")"
 
@@ -220,7 +222,7 @@
   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, existing_server: Boolean = false)
+  def init(name: String = default_name, port: Int = 0, existing_server: Boolean = false)
     : (Info, Option[Server]) =
   {
     using(SQLite.open_database(Data.database))(db =>
@@ -257,7 +259,7 @@
       })
   }
 
-  def exit(name: String = ""): Boolean =
+  def exit(name: String = default_name): Boolean =
   {
     using(SQLite.open_database(Data.database))(db =>
       db.transaction {
@@ -279,7 +281,7 @@
     {
       var console = false
       var operation_list = false
-      var name = ""
+      var name = default_name
       var port = 0
       var existing_server = false
 
@@ -290,7 +292,7 @@
   Options are:
     -C           console interaction with specified server
     -L           list servers only
-    -n NAME      explicit server name
+    -n NAME      explicit server name (default: """ + default_name + """)
     -p PORT      explicit server port
     -s           assume existing server, no implicit startup