src/Tools/VSCode/src/protocol.scala
changeset 65924 9140c9cce351
parent 65922 d2f19f05c0e9
child 65977 c51b74be23b6
equal deleted inserted replaced
65923:ab05479059b5 65924:9140c9cce351
    23 
    23 
    24     def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean)
    24     def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean)
    25     {
    25     {
    26       val header: Map[String, Any] =
    26       val header: Map[String, Any] =
    27         json match {
    27         json match {
    28           case obj: Map[Any, Any] =>
    28           case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
    29             (obj.get("method"), obj.get("id")) match {
    29             val obj = m.asInstanceOf[Map[String, JSON.T]]
    30               case (Some(method), Some(id)) => Map("method" -> method, "id" -> id)
    30             obj -- (obj.keySet - "method" - "id")
    31               case (Some(method), None) => Map("method" -> method)
       
    32               case _ => Map.empty
       
    33             }
       
    34           case _ => Map.empty
    31           case _ => Map.empty
    35         }
    32         }
    36       if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json))
    33       if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json))
    37       else logger(prefix + " " + JSON.Format(header))
    34       else logger(prefix + " " + JSON.Format(header))
    38     }
    35     }