# HG changeset patch
# User wenzelm
# Date 1551810820 -3600
# Node ID ab993a273defa6dc7be93af31a795cd13481d8c2
# Parent  3fd9298dd2008316e7c113f6579571079d529f5e
recover original order;

diff -r 3fd9298dd200 -r ab993a273def src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Tue Mar 05 18:44:02 2019 +0100
+++ b/src/Pure/General/rdf.scala	Tue Mar 05 19:33:40 2019 +0100
@@ -37,11 +37,10 @@
   }
 
   def triples(args: List[Triple]): XML.Body =
-    args.groupBy(_.subject).toList.map(
-      { case (subject, ts) =>
-          val body = XML.newline :: ts.flatMap(t => List(t.property, XML.newline))
-          description(subject, 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) })))
 
   def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
     XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)