equal
deleted
inserted
replaced
152 /* server info */ |
152 /* server info */ |
153 |
153 |
154 sealed case class Info(name: String, port: Int, password: String) |
154 sealed case class Info(name: String, port: Int, password: String) |
155 { |
155 { |
156 override def toString: String = |
156 override def toString: String = |
157 "server " + print_name_space(name) + "= " + print(port, password) |
157 "server " + quote(name) + " = " + print(port, password) |
158 |
158 |
159 def connection(): Connection = |
159 def connection(): Connection = |
160 { |
160 { |
161 val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port)) |
161 val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port)) |
162 connection.write_message(password) |
162 connection.write_message(password) |
191 } |
191 } |
192 |
192 |
193 |
193 |
194 /* per-user servers */ |
194 /* per-user servers */ |
195 |
195 |
196 def print_name_space(name: String): String = |
|
197 if (name == "") "" else quote(name) + " " |
|
198 |
|
199 def print(port: Int, password: String): String = |
196 def print(port: Int, password: String): String = |
200 "127.0.0.1:" + port + " (password " + quote(password) + ")" |
197 "127.0.0.1:" + port + " (password " + quote(password) + ")" |
201 |
198 |
202 object Data |
199 object Data |
203 { |
200 { |
237 } |
234 } |
238 db.transaction { |
235 db.transaction { |
239 find(db, name) match { |
236 find(db, name) match { |
240 case Some(server_info) => (server_info, None) |
237 case Some(server_info) => (server_info, None) |
241 case None => |
238 case None => |
242 if (existing_server) { |
239 if (existing_server) error("Isabelle server " + quote(name) + " not running") |
243 error("Isabelle server " + print_name_space(name) + "not running") |
|
244 } |
|
245 |
240 |
246 val server = new Server(port) |
241 val server = new Server(port) |
247 val server_info = Info(name, server.port, server.password) |
242 val server_info = Info(name, server.port, server.password) |
248 |
243 |
249 db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) |
244 db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) |