src/Pure/PIDE/markup.ML
changeset 70070 be04e9a053a7
parent 70068 b9985133805d
child 70098 3235ecdcd884
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun Mar 10 00:23:52 2019 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 10 14:19:30 2019 +0100
     1.3 @@ -16,6 +16,11 @@
     1.4    val serialN: string
     1.5    val serial_properties: int -> Properties.T
     1.6    val instanceN: string
     1.7 +  val meta_titleN: string val meta_title: T
     1.8 +  val meta_creatorN: string val meta_creator: T
     1.9 +  val meta_contributorN: string val meta_contributor: T
    1.10 +  val meta_dateN: string val meta_date: T
    1.11 +  val meta_descriptionN: string val meta_description: T
    1.12    val languageN: string
    1.13    val symbolsN: string
    1.14    val delimitedN: string
    1.15 @@ -283,6 +288,15 @@
    1.16  val instanceN = "instance";
    1.17  
    1.18  
    1.19 +(* meta data -- see http://dublincore.org/documents/dces *)
    1.20 +
    1.21 +val (meta_titleN, meta_title) = markup_elem "meta_title";
    1.22 +val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
    1.23 +val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
    1.24 +val (meta_dateN, meta_date) = markup_elem "meta_date";
    1.25 +val (meta_descriptionN, meta_description) = markup_elem "meta_description";
    1.26 +
    1.27 +
    1.28  (* embedded languages *)
    1.29  
    1.30  val languageN = "language";