recover original order;
authorwenzelm
Tue Mar 05 19:33:40 2019 +0100 (3 months ago ago)
changeset 70049ab993a273def
parent 70048 3fd9298dd200
child 70050 f2c3512df446
recover original order;
src/Pure/General/rdf.scala
     1.1 --- a/src/Pure/General/rdf.scala	Tue Mar 05 18:44:02 2019 +0100
     1.2 +++ b/src/Pure/General/rdf.scala	Tue Mar 05 19:33:40 2019 +0100
     1.3 @@ -37,11 +37,10 @@
     1.4    }
     1.5  
     1.6    def triples(args: List[Triple]): XML.Body =
     1.7 -    args.groupBy(_.subject).toList.map(
     1.8 -      { case (subject, ts) =>
     1.9 -          val body = XML.newline :: ts.flatMap(t => List(t.property, XML.newline))
    1.10 -          description(subject, body)
    1.11 -      })
    1.12 +    args.zipWithIndex.groupBy({ case (t, _) => t.subject }).iterator.map(_._2).
    1.13 +      toList.sortBy(ps => ps.head._2).map(ps =>
    1.14 +        description(ps.head._1.subject,
    1.15 +          XML.newline :: ps.flatMap({ case (t, _) => List(t.property, XML.newline) })))
    1.16  
    1.17    def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
    1.18      XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)