# HG changeset patch
# User wenzelm
# Date 1551874637 -3600
# Node ID 0af6b4a5a7d971431f4c250824d2a8c506f1ec73
# Parent  f2c3512df446a5b313786f59390fac120c58ccd5
afford redundant whitespace for improved readability;

diff -r f2c3512df446 -r 0af6b4a5a7d9 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)