# HG changeset patch
# User wenzelm
# Date 1495732981 -7200
# Node ID 9140c9cce3511e8af654da07821861e5a8b2cebb
# Parent  ab05479059b55bbf3a14a63b3ead4a1bfcbdb4e2
clarified output: do not require "method", which is absent for ResponseMessage;

diff -r ab05479059b5 -r 9140c9cce351 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))