# HG changeset patch
# User wenzelm
# Date 1550157912 -3600
# Node ID c64197a224c6472e844f18f478e2a5d20604fd92
# Parent  3389fda6cffdc7d6443a1bbcb2946e4592b2469f
more operations;

diff -r 3389fda6cffd -r c64197a224c6 src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Thu Feb 14 15:46:38 2019 +0100
+++ b/src/Pure/General/rdf.scala	Thu Feb 14 16:25:12 2019 +0100
@@ -39,4 +39,14 @@
 
   def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
     XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)
+
+
+  /* collections */
+
+  def collection(kind: String, items: List[XML.Body]): XML.Elem =
+    XML.elem(kind, items.map(item => XML.elem(rdf("li"), item)))
+
+  def bag(items: List[XML.Body]): XML.Elem = collection(rdf("Bag"), items)
+  def seq(items: List[XML.Body]): XML.Elem = collection(rdf("Seq"), items)
+  def alt(items: List[XML.Body]): XML.Elem = collection(rdf("Alt"), items)
 }