equal
deleted
inserted
replaced
115 /* server info */ |
115 /* server info */ |
116 |
116 |
117 sealed case class Info(name: String, port: Int, password: String) |
117 sealed case class Info(name: String, port: Int, password: String) |
118 { |
118 { |
119 override def toString: String = |
119 override def toString: String = |
120 "server " + quote(name) + " = " + print(port, password) |
120 "server " + print_name_space(name) + "= " + print(port, password) |
121 |
121 |
122 def connection(): Connection = |
122 def connection(): Connection = |
123 { |
123 { |
124 val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port)) |
124 val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port)) |
125 connection.write_message(password) |
125 connection.write_message(password) |
154 } |
154 } |
155 |
155 |
156 |
156 |
157 /* per-user servers */ |
157 /* per-user servers */ |
158 |
158 |
|
159 def print_name_space(name: String): String = |
|
160 if (name == "") "" else quote(name) + " " |
|
161 |
159 def print(port: Int, password: String): String = |
162 def print(port: Int, password: String): String = |
160 "127.0.0.1:" + port + " (password " + quote(password) + ")" |
163 "127.0.0.1:" + port + " (password " + quote(password) + ")" |
161 |
164 |
162 object Data |
165 object Data |
163 { |
166 { |
198 db.transaction { |
201 db.transaction { |
199 find(db, name) match { |
202 find(db, name) match { |
200 case Some(server_info) => (server_info, None) |
203 case Some(server_info) => (server_info, None) |
201 case None => |
204 case None => |
202 if (existing_server) { |
205 if (existing_server) { |
203 if (name == "") error("Isabelle server not running") |
206 error("Isabelle server " + print_name_space(name) + "not running") |
204 else error("Isabelle server " + quote(name) + " not running") |
|
205 } |
207 } |
206 |
208 |
207 val server = new Server(port) |
209 val server = new Server(port) |
208 val server_info = Info(name, server.port, server.password) |
210 val server_info = Info(name, server.port, server.password) |
209 |
211 |