src/Pure/General/rdf.scala
changeset 69867 3fd9298dd200
parent 69862 db622ada496d
child 69868 ab993a273def
--- a/src/Pure/General/rdf.scala	Tue Mar 05 16:40:12 2019 +0100
+++ b/src/Pure/General/rdf.scala	Tue Mar 05 18:44:02 2019 +0100
@@ -39,8 +39,7 @@
   def triples(args: List[Triple]): XML.Body =
     args.groupBy(_.subject).toList.map(
       { case (subject, ts) =>
-          val nl = XML.Text("\n")
-          val body = nl :: ts.flatMap(t => List(t.property, nl))
+          val body = XML.newline :: ts.flatMap(t => List(t.property, XML.newline))
           description(subject, body)
       })