# 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))