afford redundant whitespace for improved readability;
authorwenzelm
Wed Mar 06 13:17:17 2019 +0100 (3 months ago ago)
changeset 700510af6b4a5a7d9
parent 70050 f2c3512df446
child 70052 02e0458d342f
afford redundant whitespace for improved readability;
src/Pure/General/rdf.scala
     1.1 --- a/src/Pure/General/rdf.scala	Tue Mar 05 16:46:42 2019 +0100
     1.2 +++ b/src/Pure/General/rdf.scala	Wed Mar 06 13:17:17 2019 +0100
     1.3 @@ -37,10 +37,13 @@
     1.4    }
     1.5  
     1.6    def triples(args: List[Triple]): XML.Body =
     1.7 -    args.zipWithIndex.groupBy({ case (t, _) => t.subject }).iterator.map(_._2).
     1.8 -      toList.sortBy(ps => ps.head._2).map(ps =>
     1.9 -        description(ps.head._1.subject,
    1.10 -          XML.newline :: ps.flatMap({ case (t, _) => List(t.property, XML.newline) })))
    1.11 +    XML.newline ::
    1.12 +      args.zipWithIndex.groupBy({ case (t, _) => t.subject }).iterator.map(_._2).
    1.13 +        toList.sortBy(ps => ps.head._2).flatMap(ps =>
    1.14 +          List(
    1.15 +            description(ps.head._1.subject,
    1.16 +              XML.newline :: ps.flatMap({ case (t, _) => List(t.property, XML.newline) })),
    1.17 +            XML.newline))
    1.18  
    1.19    def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
    1.20      XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)