# HG changeset patch
# User wenzelm
# Date 1552341738 -3600
# Node ID 9c697c7ad8d61d2139579c429cf4771b78696e84
# Parent  20b32ade002469e7e7cd0687ff5a5a38d23ad48d
URIs should normally be "rdf:resource", not string body;

diff -r 20b32ade0024 -r 9c697c7ad8d6 src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Mon Mar 11 22:13:14 2019 +0100
+++ b/src/Pure/General/rdf.scala	Mon Mar 11 23:02:18 2019 +0100
@@ -9,9 +9,6 @@
 package isabelle
 
 
-import java.net.URI
-
-
 object RDF
 {
   /* document */
@@ -31,9 +28,14 @@
 
   /* multiple triples vs. compact description */
 
-  sealed case class Triple(subject: String, predicate: String, `object`: XML.Body)
+  sealed case class Triple(
+    subject: String, predicate: String, `object`: XML.Body = Nil, resource: String = "")
   {
-    def property: XML.Elem = XML.elem(predicate, `object`)
+    require(`object`.isEmpty || resource.isEmpty)
+
+    def property: XML.Elem =
+      if (resource.nonEmpty) XML.elem(Markup(predicate, List("rdf:resource" -> resource)))
+      else XML.elem(predicate, `object`)
   }
 
   def triples(args: List[Triple]): XML.Body =
@@ -65,7 +67,6 @@
   // 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))