more meta data from "dcterms" (superset of "dc");
authorwenzelm
Sun Mar 17 20:03:55 2019 +0100 (5 weeks ago)
changeset 699163235ecdcd884
parent 69915 57a41389d0e2
child 69917 66c4567664b5
more meta data from "dcterms" (superset of "dc");
src/Pure/General/rdf.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
src/Pure/Thy/document_marker.ML
     1.1 --- a/src/Pure/General/rdf.scala	Fri Mar 15 22:02:05 2019 +0100
     1.2 +++ b/src/Pure/General/rdf.scala	Sun Mar 17 20:03:55 2019 +0100
     1.3 @@ -14,9 +14,9 @@
     1.4    /* document */
     1.5  
     1.6    val rdf: XML.Namespace = XML.Namespace("rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#")
     1.7 -  val dc: XML.Namespace = XML.Namespace("dc", "http://purl.org/dc/elements/1.1/")
     1.8 +  val dcterms: XML.Namespace = XML.Namespace("dcterms", "http://purl.org/dc/terms/")
     1.9  
    1.10 -  val default_namespaces: List[XML.Namespace] = List(rdf, dc)
    1.11 +  val default_namespaces: List[XML.Namespace] = List(rdf, dcterms)
    1.12  
    1.13    def document(body: XML.Body,
    1.14      namespaces: List[XML.Namespace] = default_namespaces,
    1.15 @@ -79,11 +79,12 @@
    1.16  
    1.17    object Property  // binary relation with plain value
    1.18    {
    1.19 -    val title: String = dc("title")
    1.20 -    val creator: String = dc("creator")
    1.21 -    val contributor: String = dc("contributor")
    1.22 -    val date: String = dc("date")
    1.23 -    val description: String = dc("description")
    1.24 +    val title: String = dcterms("title")
    1.25 +    val creator: String = dcterms("creator")
    1.26 +    val contributor: String = dcterms("contributor")
    1.27 +    val date: String = dcterms("date")
    1.28 +    val description: String = dcterms("description")
    1.29 +    val license: String = dcterms("license")
    1.30    }
    1.31  
    1.32    private val meta_data_table =
    1.33 @@ -92,7 +93,8 @@
    1.34        Markup.META_CREATOR -> Property.creator,
    1.35        Markup.META_CONTRIBUTOR -> Property.contributor,
    1.36        Markup.META_DATE -> Property.date,
    1.37 -      Markup.META_DESCRIPTION -> Property.description)
    1.38 +      Markup.META_DESCRIPTION -> Property.description,
    1.39 +      Markup.META_LICENSE -> Property.license)
    1.40  
    1.41    def meta_data(props: Properties.T): Properties.T =
    1.42      props.flatMap({ case (a, b) => meta_data_table.get(a).map((_, b)) })
     2.1 --- a/src/Pure/PIDE/markup.ML	Fri Mar 15 22:02:05 2019 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 17 20:03:55 2019 +0100
     2.3 @@ -21,6 +21,7 @@
     2.4    val meta_contributorN: string val meta_contributor: T
     2.5    val meta_dateN: string val meta_date: T
     2.6    val meta_descriptionN: string val meta_description: T
     2.7 +  val meta_licenseN: string val meta_license: T
     2.8    val languageN: string
     2.9    val symbolsN: string
    2.10    val delimitedN: string
    2.11 @@ -295,6 +296,7 @@
    2.12  val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
    2.13  val (meta_dateN, meta_date) = markup_elem "meta_date";
    2.14  val (meta_descriptionN, meta_description) = markup_elem "meta_description";
    2.15 +val (meta_licenseN, meta_license) = markup_elem "meta_license";
    2.16  
    2.17  
    2.18  (* embedded languages *)
     3.1 --- a/src/Pure/PIDE/markup.scala	Fri Mar 15 22:02:05 2019 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Sun Mar 17 20:03:55 2019 +0100
     3.3 @@ -96,6 +96,7 @@
     3.4    val META_CONTRIBUTOR = "meta_contributor"
     3.5    val META_DATE = "meta_date"
     3.6    val META_DESCRIPTION = "meta_description"
     3.7 +  val META_LICENSE = "meta_license"
     3.8  
     3.9  
    3.10    /* formal entities */
     4.1 --- a/src/Pure/PIDE/rendering.scala	Fri Mar 15 22:02:05 2019 +0100
     4.2 +++ b/src/Pure/PIDE/rendering.scala	Sun Mar 17 20:03:55 2019 +0100
     4.3 @@ -210,7 +210,7 @@
     4.4  
     4.5    val meta_data_elements =
     4.6      Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR,
     4.7 -      Markup.META_DATE, Markup.META_DESCRIPTION)
     4.8 +      Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE)
     4.9  
    4.10    val markdown_elements =
    4.11      Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
     5.1 --- a/src/Pure/Thy/document_marker.ML	Fri Mar 15 22:02:05 2019 +0100
     5.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 17 20:03:55 2019 +0100
     5.3 @@ -76,7 +76,8 @@
     5.4          let
     5.5            val (arg, pos) = Input.source_content source;
     5.6            val _ = Context_Position.report ctxt pos Markup.words;
     5.7 -        in meta_data Markup.meta_description arg ctxt end));
     5.8 +        in meta_data Markup.meta_description arg ctxt end) #>
     5.9 +     setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license));
    5.10  
    5.11  fun legacy_tag name =
    5.12    Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));