src/Pure/Tools/server.scala
changeset 67911 3cda747493d8
parent 67904 465f43a9f780
child 67913 d58fa3ed236f
equal deleted inserted replaced
67906:9cc32b18c785 67911:3cda747493d8
   128     def message(msg: String, kind: String = ""): JSON.Object.T =
   128     def message(msg: String, kind: String = ""): JSON.Object.T =
   129       if (kind == "") JSON.Object("message" -> msg)
   129       if (kind == "") JSON.Object("message" -> msg)
   130       else JSON.Object(Markup.KIND -> kind, "message" -> msg)
   130       else JSON.Object(Markup.KIND -> kind, "message" -> msg)
   131 
   131 
   132     def error_message(msg: String): JSON.Object.T =
   132     def error_message(msg: String): JSON.Object.T =
   133       message(msg, kind = Markup.ERROR_MESSAGE)
   133       message(msg, kind = Markup.ERROR)
   134 
   134 
   135     def unapply(msg: String): Option[(Reply.Value, Any)] =
   135     def unapply(msg: String): Option[(Reply.Value, Any)] =
   136     {
   136     {
   137       if (msg == "") None
   137       if (msg == "") None
   138       else {
   138       else {
   223     def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
   223     def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
   224       notify(Reply.message(msg, kind = kind) ++ more)
   224       notify(Reply.message(msg, kind = kind) ++ more)
   225     def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
   225     def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
   226     def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
   226     def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
   227     def error_message(msg: String, more: JSON.Object.Entry*): Unit =
   227     def error_message(msg: String, more: JSON.Object.Entry*): Unit =
   228       message(Markup.ERROR_MESSAGE, msg, more:_*)
   228       message(Markup.ERROR, msg, more:_*)
   229 
   229 
   230     def progress(more: JSON.Object.Entry*): Connection_Progress =
   230     def progress(more: JSON.Object.Entry*): Connection_Progress =
   231       new Connection_Progress(context, more:_*)
   231       new Connection_Progress(context, more:_*)
   232 
   232 
   233     override def toString: String = connection.toString
   233     override def toString: String = connection.toString