URIs should normally be "rdf:resource", not string body;
authorwenzelm
Mon Mar 11 23:02:18 2019 +0100 (3 months ago ago)
changeset 700839c697c7ad8d6
parent 70082 20b32ade0024
child 70084 63721ee8c86c
URIs should normally be "rdf:resource", not string body;
src/Pure/General/rdf.scala
     1.1 --- a/src/Pure/General/rdf.scala	Mon Mar 11 22:13:14 2019 +0100
     1.2 +++ b/src/Pure/General/rdf.scala	Mon Mar 11 23:02:18 2019 +0100
     1.3 @@ -9,9 +9,6 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.net.URI
     1.8 -
     1.9 -
    1.10  object RDF
    1.11  {
    1.12    /* document */
    1.13 @@ -31,9 +28,14 @@
    1.14  
    1.15    /* multiple triples vs. compact description */
    1.16  
    1.17 -  sealed case class Triple(subject: String, predicate: String, `object`: XML.Body)
    1.18 +  sealed case class Triple(
    1.19 +    subject: String, predicate: String, `object`: XML.Body = Nil, resource: String = "")
    1.20    {
    1.21 -    def property: XML.Elem = XML.elem(predicate, `object`)
    1.22 +    require(`object`.isEmpty || resource.isEmpty)
    1.23 +
    1.24 +    def property: XML.Elem =
    1.25 +      if (resource.nonEmpty) XML.elem(Markup(predicate, List("rdf:resource" -> resource)))
    1.26 +      else XML.elem(predicate, `object`)
    1.27    }
    1.28  
    1.29    def triples(args: List[Triple]): XML.Body =
    1.30 @@ -65,7 +67,6 @@
    1.31    // see https://www.w3.org/TR/xmlschema-2/#built-in-datatypes
    1.32  
    1.33    def string(x: String): XML.Body = if (x.isEmpty) Nil else List(XML.Text(x))
    1.34 -  def uri(x: URI): XML.Body = string(x.toString)
    1.35    def bool(x: Boolean): XML.Body = string(x.toString)
    1.36    def int(x: Int): XML.Body = string(Value.Int(x))
    1.37    def long(x: Long): XML.Body = string(Value.Long(x))