# HG changeset patch
# User wenzelm
# Date 1484162117 -3600
# Node ID e9208a9301c08aaec3df3cf866533252ebe6154a
# Parent  31e9920a0dc1770179a86c85f83f893d98b7ef91
tuned;

diff -r 31e9920a0dc1 -r e9208a9301c0 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Wed Jan 11 20:01:55 2017 +0100
+++ b/src/Pure/General/json.scala	Wed Jan 11 20:15:17 2017 +0100
@@ -133,6 +133,12 @@
 
   /* object values */
 
+  def optional(entry: (String, Option[T])): Map[String, T] =
+    entry match {
+      case (name, Some(x)) => Map(name -> x)
+      case (_, None) => Map.empty
+    }
+
   def value(obj: T, name: String): Option[T] =
     obj match {
       case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
diff -r 31e9920a0dc1 -r e9208a9301c0 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Wed Jan 11 20:01:55 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Wed Jan 11 20:15:17 2017 +0100
@@ -100,8 +100,8 @@
   {
     def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
       Message.empty + ("id" -> id.id) ++
-      (result match { case Some(x) => Map("result" -> x) case None => Map.empty }) ++
-      (error match { case Some(x) => Map("error" -> x.json) case None => Map.empty })
+        JSON.optional("result" -> result) ++
+        JSON.optional("error" -> error.map(_.json))
 
     def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
       if (error == "") apply(id, result = result)
@@ -111,8 +111,7 @@
   sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
   {
     def json: JSON.T =
-      Map("code" -> code, "message" -> message) ++
-      (data match { case Some(x) => Map("data" -> x) case None => Map.empty })
+      Map("code" -> code, "message" -> message) ++ JSON.optional("data" -> data)
   }
 
   object ErrorCodes
@@ -305,11 +304,11 @@
   {
     def json: JSON.T =
       Message.empty + ("label" -> label) ++
-      (kind match { case Some(x) => Map("kind" -> x) case None => Map.empty }) ++
-      (detail match { case Some(x) => Map("detail" -> x) case None => Map.empty }) ++
-      (documentation match { case Some(x) => Map("documentation" -> x) case None => Map.empty }) ++
-      (insertText match { case Some(x) => Map("insertText" -> x) case None => Map.empty }) ++
-      (range match { case Some(x) => Map("range" -> Range(x)) case None => Map.empty })
+        JSON.optional("kind" -> kind) ++
+        JSON.optional("detail" -> detail) ++
+        JSON.optional("documentation" -> documentation) ++
+        JSON.optional("insertText" -> insertText) ++
+        JSON.optional("range" -> range.map(Range(_)))
   }
 
   object Completion extends RequestTextDocumentPosition("textDocument/completion")
@@ -378,9 +377,9 @@
   {
     def json: JSON.T =
       Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
-      (severity match { case Some(x) => Map("severity" -> x) case None => Map.empty }) ++
-      (code match { case Some(x) => Map("code" -> x) case None => Map.empty }) ++
-      (source match { case Some(x) => Map("source" -> x) case None => Map.empty })
+      JSON.optional("severity" -> severity) ++
+      JSON.optional("code" -> code) ++
+      JSON.optional("source" -> source)
   }
 
   object DiagnosticSeverity