# HG changeset patch
# User wenzelm
# Date 1520967898 -3600
# Node ID 5e6452a6ec896a36777f1bfb83e0d3855b921917
# Parent  3e9fe7a84b5d3c87f26378d21c2a733c84087e7e
tuned;

diff -r 3e9fe7a84b5d -r 5e6452a6ec89 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))