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]) =>