tuned signature;
authorwenzelm
Fri Oct 27 16:21:29 2017 +0200 (19 months ago)
changeset 669264cf560a6dd84
parent 66925 8b117dc73278
child 66927 153d7b68e8f8
tuned signature;
src/Pure/General/json.scala
     1.1 --- a/src/Pure/General/json.scala	Fri Oct 27 15:49:09 2017 +0200
     1.2 +++ b/src/Pure/General/json.scala	Fri Oct 27 16:21:29 2017 +0200
     1.3 @@ -257,10 +257,12 @@
     1.4  
     1.5    /* object values */
     1.6  
     1.7 +  val empty: Map[String, T] = Map.empty
     1.8 +
     1.9    def optional(entry: (String, Option[T])): Map[String, T] =
    1.10      entry match {
    1.11        case (name, Some(x)) => Map(name -> x)
    1.12 -      case (_, None) => Map.empty
    1.13 +      case (_, None) => empty
    1.14      }
    1.15  
    1.16    def value(obj: T, name: String): Option[T] =