--- 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";