# HG changeset patch
# User wenzelm
# Date 1576611287 -3600
# Node ID 93b09772666790b39cb8f6987da5e4a7da50169c
# Parent  9f2085c499a2f28d938be8d2701458089eca5b13
tuned whitespace;

diff -r 9f2085c499a2 -r 93b097726667 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Tue Dec 17 15:04:29 2019 +0100
+++ b/src/Pure/General/json.scala	Tue Dec 17 20:34:47 2019 +0100
@@ -251,7 +251,8 @@
         }
     }
 
-    object String {
+    object String
+    {
       def unapply(json: T): Option[java.lang.String] =
         json match {
           case x: java.lang.String => Some(x)
@@ -259,7 +260,8 @@
         }
     }
 
-    object Double {
+    object Double
+    {
       def unapply(json: T): Option[scala.Double] =
         json match {
           case x: scala.Double => Some(x)
@@ -269,7 +271,8 @@
         }
     }
 
-    object Long {
+    object Long
+    {
       def unapply(json: T): Option[scala.Long] =
         json match {
           case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong)
@@ -279,7 +282,8 @@
         }
     }
 
-    object Int {
+    object Int
+    {
       def unapply(json: T): Option[scala.Int] =
         json match {
           case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt)
@@ -289,7 +293,8 @@
         }
     }
 
-    object Boolean {
+    object Boolean
+    {
       def unapply(json: T): Option[scala.Boolean] =
         json match {
           case x: scala.Boolean => Some(x)
@@ -308,7 +313,8 @@
         }
     }
 
-    object Seconds {
+    object Seconds
+    {
       def unapply(json: T): Option[Time] =
         Double.unapply(json).map(Time.seconds(_))
     }