src/Pure/Tools/server.scala

--- a/src/Pure/Tools/server.scala	Fri Mar 09 12:42:34 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 12:45:53 2018 +0100
@@ -113,7 +113,7 @@
   def find(db: SQLite.Database, name: String): Option[Data.Entry] =
     list(db).find(entry => entry.name == name && entry.active)
 
-  def start(name: String = "", port: Int = 0): (Data.Entry, Option[Server]) =
+  def init(name: String = "", port: Int = 0): (Data.Entry, Option[Server]) =
   {
     using(SQLite.open_database(Data.database))(db =>
       db.transaction {
@@ -139,7 +139,7 @@
       })
   }
 
-  def stop(name: String = ""): Boolean =
+  def exit(name: String = ""): Boolean =
   {
     using(SQLite.open_database(Data.database))(db =>
       db.transaction {
@@ -190,7 +190,7 @@
           Output.writeln(entry.toString, stdout = true)
       }
       else {
-        val (entry, server) = start(name, port)
+        val (entry, server) = init(name, port)
         Output.writeln(entry.toString, stdout = true)
         server.foreach(_.join)
       }