afford redundant whitespace for improved readability;
authorwenzelm
Wed, 06 Mar 2019 13:17:17 +0100
changeset 69870 0af6b4a5a7d9
parent 69869 f2c3512df446
child 69871 02e0458d342f
afford redundant whitespace for improved readability;
src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Tue Mar 05 16:46:42 2019 +0100
+++ b/src/Pure/General/rdf.scala	Wed Mar 06 13:17:17 2019 +0100
@@ -37,10 +37,13 @@
   }
 
   def triples(args: List[Triple]): XML.Body =
-    args.zipWithIndex.groupBy({ case (t, _) => t.subject }).iterator.map(_._2).
-      toList.sortBy(ps => ps.head._2).map(ps =>
-        description(ps.head._1.subject,
-          XML.newline :: ps.flatMap({ case (t, _) => List(t.property, XML.newline) })))
+    XML.newline ::
+      args.zipWithIndex.groupBy({ case (t, _) => t.subject }).iterator.map(_._2).
+        toList.sortBy(ps => ps.head._2).flatMap(ps =>
+          List(
+            description(ps.head._1.subject,
+              XML.newline :: ps.flatMap({ case (t, _) => List(t.property, XML.newline) })),
+            XML.newline))
 
   def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
     XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)