src/Pure/PIDE/markup.ML
changeset 70098 3235ecdcd884
parent 70070 be04e9a053a7
child 70144 82e945d472d5
     1.1 --- a/src/Pure/PIDE/markup.ML	Fri Mar 15 22:02:05 2019 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 17 20:03:55 2019 +0100
     1.3 @@ -21,6 +21,7 @@
     1.4    val meta_contributorN: string val meta_contributor: T
     1.5    val meta_dateN: string val meta_date: T
     1.6    val meta_descriptionN: string val meta_description: T
     1.7 +  val meta_licenseN: string val meta_license: T
     1.8    val languageN: string
     1.9    val symbolsN: string
    1.10    val delimitedN: string
    1.11 @@ -295,6 +296,7 @@
    1.12  val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
    1.13  val (meta_dateN, meta_date) = markup_elem "meta_date";
    1.14  val (meta_descriptionN, meta_description) = markup_elem "meta_description";
    1.15 +val (meta_licenseN, meta_license) = markup_elem "meta_license";
    1.16  
    1.17  
    1.18  (* embedded languages *)