clarified signature;
authorwenzelm
Tue, 13 Mar 2018 10:54:40 +0100
changeset 67842 ff87225e7e8e
parent 67841 8ada8f6d9495
child 67843 ff561f6e0a8e
clarified signature;
src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Mon Mar 12 18:33:30 2018 +0100
+++ b/src/Pure/General/json.scala	Tue Mar 13 10:54:40 2018 +0100
@@ -232,10 +232,18 @@
   }
 
 
-  /* numbers */
+  /* values */
 
-  object Number
+  object Value
   {
+    object String {
+      def unapply(json: T): Option[java.lang.String] =
+        json match {
+          case x: java.lang.String => Some(x)
+          case _ => None
+        }
+    }
+
     object Double {
       def unapply(json: T): Option[scala.Double] =
         json match {
@@ -265,6 +273,14 @@
           case _ => None
         }
     }
+
+    object Boolean {
+      def unapply(json: T): Option[scala.Boolean] =
+        json match {
+          case x: scala.Boolean => Some(x)
+          case _ => None
+        }
+    }
   }
 
 
@@ -302,23 +318,17 @@
     } yield a.map(_.get)
 
   def string(obj: T, name: String): Option[String] =
-    value(obj, name) match {
-      case Some(x: String) => Some(x)
-      case _ => None
-    }
+    value(obj, name, Value.String.unapply)
 
   def double(obj: T, name: String): Option[Double] =
-    value(obj, name, Number.Double.unapply)
+    value(obj, name, Value.Double.unapply)
 
   def long(obj: T, name: String): Option[Long] =
-    value(obj, name, Number.Long.unapply)
+    value(obj, name, Value.Long.unapply)
 
   def int(obj: T, name: String): Option[Int] =
-    value(obj, name, Number.Int.unapply)
+    value(obj, name, Value.Int.unapply)
 
   def bool(obj: T, name: String): Option[Boolean] =
-    value(obj, name) match {
-      case Some(x: Boolean) => Some(x)
-      case _ => None
-    }
+    value(obj, name, Value.Boolean.unapply)
 }