# HG changeset patch
# User wenzelm
# Date 1553539852 -3600
# Node ID f150253cb201933862e42589ede8acc3e9e5aab2
# Parent  3dced198b9ec44da5084352b90d5c6cc6a1373c3
RDF meta data for AFP entries;
tuned;

diff -r 3dced198b9ec -r f150253cb201 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Mar 25 17:21:26 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 19:50:52 2019 +0100
@@ -50,6 +50,15 @@
     def maintainers: List[String] = get_strings("notify")
     def contributors: List[String] = get_strings("contributors")
     def license: String = get("license").getOrElse("BSD")
+
+    def rdf_meta_data: Properties.T =
+      RDF.meta_data(
+        proper_string(title).map(Markup.META_TITLE -> _).toList :::
+        authors.map(Markup.META_CREATOR -> _) :::
+        contributors.map(Markup.META_CONTRIBUTOR -> _) :::
+        List(Markup.META_DATE -> RDF.date_format(date)) :::
+        List(Markup.META_LICENSE -> license) :::
+        proper_string(`abstract`).map(Markup.META_DESCRIPTION -> _).toList)
   }
 }
 
diff -r 3dced198b9ec -r f150253cb201 src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Mon Mar 25 17:21:26 2019 +0100
+++ b/src/Pure/General/rdf.scala	Mon Mar 25 19:50:52 2019 +0100
@@ -72,7 +72,9 @@
   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))
+
+  val date_format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ss.SSSxxx")
+  def date_time_stamp(x: Date): XML.Body = string(date_format(x))
 
 
   /* predicates */
@@ -83,8 +85,8 @@
     val creator: String = dcterms("creator")
     val contributor: String = dcterms("contributor")
     val date: String = dcterms("date")
+    val license: String = dcterms("license")
     val description: String = dcterms("description")
-    val license: String = dcterms("license")
   }
 
   private val meta_data_table =
@@ -93,8 +95,8 @@
       Markup.META_CREATOR -> Property.creator,
       Markup.META_CONTRIBUTOR -> Property.contributor,
       Markup.META_DATE -> Property.date,
-      Markup.META_DESCRIPTION -> Property.description,
-      Markup.META_LICENSE -> Property.license)
+      Markup.META_LICENSE -> Property.license,
+      Markup.META_DESCRIPTION -> Property.description)
 
   def meta_data(props: Properties.T): Properties.T =
     props.flatMap({ case (a, b) => meta_data_table.get(a).map((_, b)) })