more meta data from "dcterms" (superset of "dc");

--- a/src/Pure/General/rdf.scala	Fri Mar 15 22:02:05 2019 +0100
+++ b/src/Pure/General/rdf.scala	Sun Mar 17 20:03:55 2019 +0100
@@ -14,9 +14,9 @@
   /* document */
 
   val rdf: XML.Namespace = XML.Namespace("rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#")
-  val dc: XML.Namespace = XML.Namespace("dc", "http://purl.org/dc/elements/1.1/")
+  val dcterms: XML.Namespace = XML.Namespace("dcterms", "http://purl.org/dc/terms/")
 
-  val default_namespaces: List[XML.Namespace] = List(rdf, dc)
+  val default_namespaces: List[XML.Namespace] = List(rdf, dcterms)
 
   def document(body: XML.Body,
     namespaces: List[XML.Namespace] = default_namespaces,
@@ -79,11 +79,12 @@
 
   object Property  // binary relation with plain value
   {
-    val title: String = dc("title")
-    val creator: String = dc("creator")
-    val contributor: String = dc("contributor")
-    val date: String = dc("date")
-    val description: String = dc("description")
+    val title: String = dcterms("title")
+    val creator: String = dcterms("creator")
+    val contributor: String = dcterms("contributor")
+    val date: String = dcterms("date")
+    val description: String = dcterms("description")
+    val license: String = dcterms("license")
   }
 
   private val meta_data_table =
@@ -92,7 +93,8 @@
       Markup.META_CREATOR -> Property.creator,
       Markup.META_CONTRIBUTOR -> Property.contributor,
       Markup.META_DATE -> Property.date,
-      Markup.META_DESCRIPTION -> Property.description)
+      Markup.META_DESCRIPTION -> Property.description,
+      Markup.META_LICENSE -> Property.license)
 
   def meta_data(props: Properties.T): Properties.T =
     props.flatMap({ case (a, b) => meta_data_table.get(a).map((_, b)) })

--- a/src/Pure/PIDE/markup.ML	Fri Mar 15 22:02:05 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Mar 17 20:03:55 2019 +0100
@@ -21,6 +21,7 @@
   val meta_contributorN: string val meta_contributor: T
   val meta_dateN: string val meta_date: T
   val meta_descriptionN: string val meta_description: T
+  val meta_licenseN: string val meta_license: T
   val languageN: string
   val symbolsN: string
   val delimitedN: string
@@ -295,6 +296,7 @@
 val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
 val (meta_dateN, meta_date) = markup_elem "meta_date";
 val (meta_descriptionN, meta_description) = markup_elem "meta_description";
+val (meta_licenseN, meta_license) = markup_elem "meta_license";
 
 
 (* embedded languages *)

--- a/src/Pure/PIDE/markup.scala	Fri Mar 15 22:02:05 2019 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Mar 17 20:03:55 2019 +0100
@@ -96,6 +96,7 @@
   val META_CONTRIBUTOR = "meta_contributor"
   val META_DATE = "meta_date"
   val META_DESCRIPTION = "meta_description"
+  val META_LICENSE = "meta_license"
 
 
   /* formal entities */

--- a/src/Pure/PIDE/rendering.scala	Fri Mar 15 22:02:05 2019 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Mar 17 20:03:55 2019 +0100
@@ -210,7 +210,7 @@
 
   val meta_data_elements =
     Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR,
-      Markup.META_DATE, Markup.META_DESCRIPTION)
+      Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE)
 
   val markdown_elements =
     Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,

--- a/src/Pure/Thy/document_marker.ML	Fri Mar 15 22:02:05 2019 +0100
+++ b/src/Pure/Thy/document_marker.ML	Sun Mar 17 20:03:55 2019 +0100
@@ -76,7 +76,8 @@
         let
           val (arg, pos) = Input.source_content source;
           val _ = Context_Position.report ctxt pos Markup.words;
-        in meta_data Markup.meta_description arg ctxt end));
+        in meta_data Markup.meta_description arg ctxt end) #>
+     setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license));
 
 fun legacy_tag name =
   Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));