src/Pure/General/graph.scala
changeset 75394 42267c650205
parent 75393 87ebf5a50283
child 76840 893eeef9ef08
--- a/src/Pure/General/graph.scala	Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/graph.scala	Fri Apr 01 23:19:12 2022 +0200
@@ -52,14 +52,14 @@
   /* XML data representation */
 
   def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] =
-    (graph: Graph[Key, A]) => {
+    { (graph: Graph[Key, A]) =>
       import XML.Encode._
       list(pair(pair(key, info), list(key)))(graph.dest)
     }
 
   def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(
     implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
-    (body: XML.Body) => {
+    { (body: XML.Body) =>
       import XML.Decode._
       make(list(pair(pair(key, info), list(key)))(body))(ord)
     }