src/Pure/PIDE/markup.scala
changeset 70070 be04e9a053a7
parent 69967 c175499a7537
child 70098 3235ecdcd884
     1.1 --- a/src/Pure/PIDE/markup.scala	Sun Mar 10 00:23:52 2019 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sun Mar 10 14:19:30 2019 +0100
     1.3 @@ -89,6 +89,15 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* meta data */
     1.8 +
     1.9 +  val META_TITLE = "meta_title"
    1.10 +  val META_CREATOR = "meta_creator"
    1.11 +  val META_CONTRIBUTOR = "meta_contributor"
    1.12 +  val META_DATE = "meta_date"
    1.13 +  val META_DESCRIPTION = "meta_description"
    1.14 +
    1.15 +
    1.16    /* formal entities */
    1.17  
    1.18    val BINDING = "binding"