183 |
183 |
184 def read_password(password: String): Boolean = |
184 def read_password(password: String): Boolean = |
185 try { Byte_Message.read_line(in).map(_.text) == Some(password) } |
185 try { Byte_Message.read_line(in).map(_.text) == Some(password) } |
186 catch { case _: IOException => false } |
186 catch { case _: IOException => false } |
187 |
187 |
188 def read_message(): Option[String] = |
188 def read_line_message(): Option[String] = |
189 try { Byte_Message.read_line_message(in).map(_.text) } |
189 try { Byte_Message.read_line_message(in).map(_.text) } |
190 catch { case _: IOException => None } |
190 catch { case _: IOException => None } |
191 |
191 |
192 def await_close(): Unit = |
192 def await_close(): Unit = |
193 try { Byte_Message.read(in, 1); socket.close() } |
193 try { Byte_Message.read(in, 1); socket.close() } |
194 catch { case _: IOException => } |
194 catch { case _: IOException => } |
195 |
195 |
196 def write_message(msg: String): Unit = |
196 def write_line_message(msg: String): Unit = |
197 out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) } |
197 out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) } |
198 |
198 |
199 def reply(r: Reply.Value, arg: Any): Unit = |
199 def reply(r: Reply.Value, arg: Any): Unit = |
200 { |
200 { |
201 val argument = Argument.print(arg) |
201 val argument = Argument.print(arg) |
202 write_message(if (argument == "") r.toString else r.toString + " " + argument) |
202 write_line_message(if (argument == "") r.toString else r.toString + " " + argument) |
203 } |
203 } |
204 |
204 |
205 def reply_ok(arg: Any): Unit = reply(Reply.OK, arg) |
205 def reply_ok(arg: Any): Unit = reply(Reply.OK, arg) |
206 def reply_error(arg: Any): Unit = reply(Reply.ERROR, arg) |
206 def reply_error(arg: Any): Unit = reply(Reply.ERROR, arg) |
207 def reply_error_message(message: String, more: JSON.Object.Entry*): Unit = |
207 def reply_error_message(message: String, more: JSON.Object.Entry*): Unit = |
345 "server " + quote(name) + " = " + print(port, password) |
345 "server " + quote(name) + " = " + print(port, password) |
346 |
346 |
347 def connection(): Connection = |
347 def connection(): Connection = |
348 { |
348 { |
349 val connection = Connection(new Socket(localhost, port)) |
349 val connection = Connection(new Socket(localhost, port)) |
350 connection.write_message(password) |
350 connection.write_line_message(password) |
351 connection |
351 connection |
352 } |
352 } |
353 |
353 |
354 def active: Boolean = |
354 def active: Boolean = |
355 try { |
355 try { |
356 using(connection())(connection => |
356 using(connection())(connection => |
357 { |
357 { |
358 connection.set_timeout(Time.seconds(2.0)) |
358 connection.set_timeout(Time.seconds(2.0)) |
359 connection.read_message() match { |
359 connection.read_line_message() match { |
360 case Some(Reply(Reply.OK, _)) => true |
360 case Some(Reply(Reply.OK, _)) => true |
361 case _ => false |
361 case _ => false |
362 } |
362 } |
363 }) |
363 }) |
364 } |
364 } |
442 { |
442 { |
443 using(SQLite.open_database(Data.database))(db => |
443 using(SQLite.open_database(Data.database))(db => |
444 db.transaction { |
444 db.transaction { |
445 find(db, name) match { |
445 find(db, name) match { |
446 case Some(server_info) => |
446 case Some(server_info) => |
447 using(server_info.connection())(_.write_message("shutdown")) |
447 using(server_info.connection())(_.write_line_message("shutdown")) |
448 while(server_info.active) { Time.seconds(0.05).sleep() } |
448 while(server_info.active) { Time.seconds(0.05).sleep() } |
449 true |
449 true |
450 case None => false |
450 case None => false |
451 } |
451 } |
452 }) |
452 }) |
557 "isabelle_id" -> Isabelle_System.isabelle_id(), |
557 "isabelle_id" -> Isabelle_System.isabelle_id(), |
558 "isabelle_name" -> Isabelle_System.isabelle_name())) |
558 "isabelle_name" -> Isabelle_System.isabelle_name())) |
559 |
559 |
560 var finished = false |
560 var finished = false |
561 while (!finished) { |
561 while (!finished) { |
562 connection.read_message() match { |
562 connection.read_line_message() match { |
563 case None => finished = true |
563 case None => finished = true |
564 case Some("") => context.notify("Command 'help' provides list of commands") |
564 case Some("") => context.notify("Command 'help' provides list of commands") |
565 case Some(msg) => |
565 case Some(msg) => |
566 val (name, argument) = Server.Argument.split(msg) |
566 val (name, argument) = Server.Argument.split(msg) |
567 Server.command_table.get(name) match { |
567 Server.command_table.get(name) match { |