more explicit error messages;
authorwenzelm
Sun Mar 18 12:11:30 2018 +0100 (14 months ago)
changeset 679013e6864cf387f
parent 67900 5a1b0076d7f0
child 67902 c88044b10bbf
more explicit error messages;
clarified signature;
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/Tools/server.scala	Sun Mar 18 11:42:57 2018 +0100
     1.2 +++ b/src/Pure/Tools/server.scala	Sun Mar 18 12:11:30 2018 +0100
     1.3 @@ -113,9 +113,9 @@
     1.4  
     1.5    def json_error(exn: Throwable): JSON.Object.T =
     1.6      exn match {
     1.7 -      case ERROR(msg) => JSON.Object(Reply.message(msg))
     1.8 -      case e: Error => JSON.Object(Reply.message(e.message)) ++ e.json
     1.9 -      case _ if Exn.is_interrupt(exn) => JSON.Object(Reply.message(Exn.message(exn)))
    1.10 +      case ERROR(msg) => Reply.error_message(msg)
    1.11 +      case e: Error => Reply.error_message(e.message) ++ e.json
    1.12 +      case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
    1.13        case _ => JSON.Object.empty
    1.14      }
    1.15  
    1.16 @@ -123,7 +123,12 @@
    1.17    {
    1.18      val OK, ERROR, FINISHED, FAILED, NOTE = Value
    1.19  
    1.20 -    def message(msg: String): JSON.Object.Entry = ("message" -> msg)
    1.21 +    def message(msg: String, kind: String = ""): JSON.Object.T =
    1.22 +      if (kind == "") JSON.Object("message" -> msg)
    1.23 +      else JSON.Object(Markup.KIND -> kind, "message" -> msg)
    1.24 +
    1.25 +    def error_message(msg: String): JSON.Object.T =
    1.26 +      message(msg, kind = Markup.ERROR_MESSAGE)
    1.27  
    1.28      def unapply(msg: String): Option[(Reply.Value, Any)] =
    1.29      {
    1.30 @@ -199,7 +204,7 @@
    1.31      def reply_ok(arg: Any) { reply(Reply.OK, arg) }
    1.32      def reply_error(arg: Any) { reply(Reply.ERROR, arg) }
    1.33      def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
    1.34 -      reply_error(JSON.Object(Reply.message(message)) ++ more)
    1.35 +      reply_error(Reply.error_message(message) ++ more)
    1.36  
    1.37      def notify(arg: Any) { reply(Reply.NOTE, arg) }
    1.38    }
    1.39 @@ -214,7 +219,7 @@
    1.40      def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
    1.41      def notify(arg: Any) { connection.notify(arg) }
    1.42      def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
    1.43 -      notify(JSON.Object(Markup.KIND -> kind, Reply.message(msg)) ++ more)
    1.44 +      notify(Reply.message(msg, kind = kind) ++ more)
    1.45      def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
    1.46      def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
    1.47      def error_message(msg: String, more: JSON.Object.Entry*): Unit =
     2.1 --- a/src/Pure/Tools/server_commands.scala	Sun Mar 18 11:42:57 2018 +0100
     2.2 +++ b/src/Pure/Tools/server_commands.scala	Sun Mar 18 12:11:30 2018 +0100
     2.3 @@ -186,20 +186,18 @@
     2.4          session.use_theories(args.theories, qualifier = args.qualifier,
     2.5            master_dir = args.master_dir, id = id, progress = progress)
     2.6  
     2.7 -      def output_text(s: String): JSON.Object.Entry =
     2.8 -        Server.Reply.message(if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s))
     2.9 +      def output_text(s: String): String =
    2.10 +        if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
    2.11  
    2.12        def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
    2.13        {
    2.14          val position = "pos" -> Position.JSON(pos)
    2.15          tree match {
    2.16 -          case XML.Text(msg) => JSON.Object(output_text(msg), position)
    2.17 +          case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
    2.18            case elem: XML.Elem =>
    2.19              val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
    2.20 -            Markup.messages.collectFirst({ case (a, b) if b == elem.name => a }) match {
    2.21 -              case None => JSON.Object(output_text(msg), position)
    2.22 -              case Some(kind) => JSON.Object(Markup.KIND -> kind, output_text(msg), position)
    2.23 -            }
    2.24 +            val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => a })
    2.25 +            Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position
    2.26          }
    2.27        }
    2.28