# HG changeset patch
# User wenzelm
# Date 1509114089 -7200
# Node ID 4cf560a6dd8492b7fcc8dbcefe853f708c83512d
# Parent  8b117dc73278d94979bbffe6b9953f97972d241d
tuned signature;

diff -r 8b117dc73278 -r 4cf560a6dd84 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Fri Oct 27 15:49:09 2017 +0200
+++ b/src/Pure/General/json.scala	Fri Oct 27 16:21:29 2017 +0200
@@ -257,10 +257,12 @@
 
   /* object values */
 
+  val empty: Map[String, T] = Map.empty
+
   def optional(entry: (String, Option[T])): Map[String, T] =
     entry match {
       case (name, Some(x)) => Map(name -> x)
-      case (_, None) => Map.empty
+      case (_, None) => empty
     }
 
   def value(obj: T, name: String): Option[T] =