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