# HG changeset patch
# User wenzelm
# Date 1550179146 -3600
# Node ID 028f61045e8d67e9e514845ebed65133aaaa29f8
# Parent  c64197a224c6472e844f18f478e2a5d20604fd92
more operations;

diff -r c64197a224c6 -r 028f61045e8d src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Thu Feb 14 16:25:12 2019 +0100
+++ b/src/Pure/General/rdf.scala	Thu Feb 14 22:19:06 2019 +0100
@@ -9,6 +9,9 @@
 package isabelle
 
 
+import java.net.URI
+
+
 object RDF
 {
   /* document */
@@ -49,4 +52,19 @@
   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)
+
+
+  /* datatypes */
+
+  // see https://www.w3.org/TR/rdf11-concepts/#section-Datatypes
+  // see https://www.w3.org/TR/xmlschema-2/#built-in-datatypes
+
+  def string(x: String): XML.Body = if (x.isEmpty) Nil else List(XML.Text(x))
+  def uri(x: URI): XML.Body = string(x.toString)
+  def bool(x: Boolean): XML.Body = string(x.toString)
+  def int(x: Int): XML.Body = string(Value.Int(x))
+  def long(x: Long): XML.Body = string(Value.Long(x))
+  def double(x: Double): XML.Body = string(Value.Double(x))
+  def seconds(x: Time): XML.Body = double(x.seconds)
+  def date_time_stamp(x: Date): XML.Body = string(Date.Format("uuuu-MM-dd'T'HH:mm:ss.SSSxxx")(x))
 }