tuned;
authorwenzelm
Tue, 13 Mar 2018 20:04:58 +0100
changeset 67851 5e6452a6ec89
parent 67850 3e9fe7a84b5d
child 67852 f701a1d5d852
tuned;
src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Tue Mar 13 20:02:09 2018 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Tue Mar 13 20:04:58 2018 +0100
@@ -23,11 +23,9 @@
 
     def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean)
     {
-      val header: Map[String, Any] =
+      val header =
         json match {
-          case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
-            val obj = m.asInstanceOf[Map[String, JSON.T]]
-            obj -- (obj.keySet - "method" - "id")
+          case JSON.Object(obj) => obj -- (obj.keySet - "method" - "id")
           case _ => JSON.Object.empty
         }
       if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json))