markup and document markers for some meta data from "Dublin Core Metadata Element Set";

--- a/src/Pure/PIDE/markup.ML	Sun Mar 10 00:23:52 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Mar 10 14:19:30 2019 +0100
@@ -16,6 +16,11 @@
   val serialN: string
   val serial_properties: int -> Properties.T
   val instanceN: string
+  val meta_titleN: string val meta_title: T
+  val meta_creatorN: string val meta_creator: T
+  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 languageN: string
   val symbolsN: string
   val delimitedN: string
@@ -283,6 +288,15 @@
 val instanceN = "instance";
 
 
+(* meta data -- see http://dublincore.org/documents/dces *)
+
+val (meta_titleN, meta_title) = markup_elem "meta_title";
+val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
+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";
+
+
 (* embedded languages *)
 
 val languageN = "language";

--- a/src/Pure/PIDE/markup.scala	Sun Mar 10 00:23:52 2019 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Mar 10 14:19:30 2019 +0100
@@ -89,6 +89,15 @@
   }
 
 
+  /* meta data */
+
+  val META_TITLE = "meta_title"
+  val META_CREATOR = "meta_creator"
+  val META_CONTRIBUTOR = "meta_contributor"
+  val META_DATE = "meta_date"
+  val META_DESCRIPTION = "meta_description"
+
+
   /* formal entities */
 
   val BINDING = "binding"

--- a/src/Pure/Thy/document_marker.ML	Sun Mar 10 00:23:52 2019 +0100
+++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 14:19:30 2019 +0100
@@ -8,6 +8,7 @@
 sig
   type marker = Proof.context -> Proof.context
   val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
+  val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
   val evaluate: Input.source -> marker
 end;
 
@@ -37,6 +38,8 @@
       in body x ctxt' end;
   in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;
 
+fun setup0 name scan = setup name (Scan.lift scan);
+
 
 (* evaluate inner syntax *)
 
@@ -57,8 +60,16 @@
 
 (* concrete markers *)
 
+fun meta_data markup arg ctxt =
+  (Context_Position.report_text ctxt (Position.thread_data ()) markup arg; ctxt);
+
 val _ =
   Theory.setup
-    (setup (Binding.make ("tag", \<^here>)) (Scan.lift Parse.name) Document_Source.update_tags);
+    (setup0 (Binding.make ("tag", \<^here>)) Parse.name Document_Source.update_tags #>
+     setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #>
+     setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
+     setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
+     setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
+     setup0 (Binding.make ("description", \<^here>)) Parse.embedded (meta_data Markup.meta_description));
 
 end;