clarified output: do not require "method", which is absent for ResponseMessage;
authorwenzelm
Thu, 25 May 2017 19:23:01 +0200
changeset 65924 9140c9cce351
parent 65923 ab05479059b5
child 65925 4a1b666b6362
clarified output: do not require "method", which is absent for ResponseMessage;
src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Thu May 25 18:13:16 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Thu May 25 19:23:01 2017 +0200
@@ -25,12 +25,9 @@
     {
       val header: Map[String, Any] =
         json match {
-          case obj: Map[Any, Any] =>
-            (obj.get("method"), obj.get("id")) match {
-              case (Some(method), Some(id)) => Map("method" -> method, "id" -> id)
-              case (Some(method), None) => Map("method" -> method)
-              case _ => Map.empty
-            }
+          case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
+            val obj = m.asInstanceOf[Map[String, JSON.T]]
+            obj -- (obj.keySet - "method" - "id")
           case _ => Map.empty
         }
       if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json))