src/Pure/General/rdf.scala
changeset 69808 c64197a224c6
parent 69807 3389fda6cffd
child 69809 028f61045e8d
equal deleted inserted replaced
69807:3389fda6cffd 69808:c64197a224c6
    37     args.groupBy(_.subject).toList.map(
    37     args.groupBy(_.subject).toList.map(
    38       { case (subject, ts) => description(subject, ts.map(_.property)) })
    38       { case (subject, ts) => description(subject, ts.map(_.property)) })
    39 
    39 
    40   def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
    40   def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
    41     XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)
    41     XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)
       
    42 
       
    43 
       
    44   /* collections */
       
    45 
       
    46   def collection(kind: String, items: List[XML.Body]): XML.Elem =
       
    47     XML.elem(kind, items.map(item => XML.elem(rdf("li"), item)))
       
    48 
       
    49   def bag(items: List[XML.Body]): XML.Elem = collection(rdf("Bag"), items)
       
    50   def seq(items: List[XML.Body]): XML.Elem = collection(rdf("Seq"), items)
       
    51   def alt(items: List[XML.Body]): XML.Elem = collection(rdf("Alt"), items)
    42 }
    52 }