# 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)) }