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) })