src/Pure/PIDE/markup.scala
changeset 69916 3235ecdcd884
parent 69889 be04e9a053a7
child 69962 82e945d472d5
equal deleted inserted replaced
69915:57a41389d0e2 69916:3235ecdcd884
    94   val META_TITLE = "meta_title"
    94   val META_TITLE = "meta_title"
    95   val META_CREATOR = "meta_creator"
    95   val META_CREATOR = "meta_creator"
    96   val META_CONTRIBUTOR = "meta_contributor"
    96   val META_CONTRIBUTOR = "meta_contributor"
    97   val META_DATE = "meta_date"
    97   val META_DATE = "meta_date"
    98   val META_DESCRIPTION = "meta_description"
    98   val META_DESCRIPTION = "meta_description"
       
    99   val META_LICENSE = "meta_license"
    99 
   100 
   100 
   101 
   101   /* formal entities */
   102   /* formal entities */
   102 
   103 
   103   val BINDING = "binding"
   104   val BINDING = "binding"