RDF meta data for AFP entries;
authorwenzelm
Mon Mar 25 19:50:52 2019 +0100 (8 weeks ago)
changeset 69982f150253cb201
parent 69981 3dced198b9ec
child 69983 4ce5ce3a612b
RDF meta data for AFP entries;
tuned;
src/Pure/Admin/afp.scala
src/Pure/General/rdf.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Mar 25 17:21:26 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 19:50:52 2019 +0100
     1.3 @@ -50,6 +50,15 @@
     1.4      def maintainers: List[String] = get_strings("notify")
     1.5      def contributors: List[String] = get_strings("contributors")
     1.6      def license: String = get("license").getOrElse("BSD")
     1.7 +
     1.8 +    def rdf_meta_data: Properties.T =
     1.9 +      RDF.meta_data(
    1.10 +        proper_string(title).map(Markup.META_TITLE -> _).toList :::
    1.11 +        authors.map(Markup.META_CREATOR -> _) :::
    1.12 +        contributors.map(Markup.META_CONTRIBUTOR -> _) :::
    1.13 +        List(Markup.META_DATE -> RDF.date_format(date)) :::
    1.14 +        List(Markup.META_LICENSE -> license) :::
    1.15 +        proper_string(`abstract`).map(Markup.META_DESCRIPTION -> _).toList)
    1.16    }
    1.17  }
    1.18  
     2.1 --- a/src/Pure/General/rdf.scala	Mon Mar 25 17:21:26 2019 +0100
     2.2 +++ b/src/Pure/General/rdf.scala	Mon Mar 25 19:50:52 2019 +0100
     2.3 @@ -72,7 +72,9 @@
     2.4    def long(x: Long): XML.Body = string(Value.Long(x))
     2.5    def double(x: Double): XML.Body = string(Value.Double(x))
     2.6    def seconds(x: Time): XML.Body = double(x.seconds)
     2.7 -  def date_time_stamp(x: Date): XML.Body = string(Date.Format("uuuu-MM-dd'T'HH:mm:ss.SSSxxx")(x))
     2.8 +
     2.9 +  val date_format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ss.SSSxxx")
    2.10 +  def date_time_stamp(x: Date): XML.Body = string(date_format(x))
    2.11  
    2.12  
    2.13    /* predicates */
    2.14 @@ -83,8 +85,8 @@
    2.15      val creator: String = dcterms("creator")
    2.16      val contributor: String = dcterms("contributor")
    2.17      val date: String = dcterms("date")
    2.18 +    val license: String = dcterms("license")
    2.19      val description: String = dcterms("description")
    2.20 -    val license: String = dcterms("license")
    2.21    }
    2.22  
    2.23    private val meta_data_table =
    2.24 @@ -93,8 +95,8 @@
    2.25        Markup.META_CREATOR -> Property.creator,
    2.26        Markup.META_CONTRIBUTOR -> Property.contributor,
    2.27        Markup.META_DATE -> Property.date,
    2.28 -      Markup.META_DESCRIPTION -> Property.description,
    2.29 -      Markup.META_LICENSE -> Property.license)
    2.30 +      Markup.META_LICENSE -> Property.license,
    2.31 +      Markup.META_DESCRIPTION -> Property.description)
    2.32  
    2.33    def meta_data(props: Properties.T): Properties.T =
    2.34      props.flatMap({ case (a, b) => meta_data_table.get(a).map((_, b)) })