diff -r 34e76587dc94 -r 77a65c9a849a 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) }