src/Pure/PIDE/markup.scala
changeset 67336 3ee6da378183
parent 67323 d02208cefbdb
child 67839 0c2ed45ece20
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Jan 03 11:06:41 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jan 03 20:55:13 2018 +0100
     1.3 @@ -161,6 +161,7 @@
     1.4    val LANGUAGE = "language"
     1.5    object Language
     1.6    {
     1.7 +    val DOCUMENT = "document"
     1.8      val ML = "ML"
     1.9      val SML = "SML"
    1.10      val PATH = "path"
    1.11 @@ -297,8 +298,12 @@
    1.12  
    1.13    val MARKDOWN_PARAGRAPH = "markdown_paragraph"
    1.14    val MARKDOWN_ITEM = "markdown_item"
    1.15 +  val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
    1.16    val Markdown_List = new Markup_String("markdown_list", "kind")
    1.17 -  val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
    1.18 +
    1.19 +  val ITEMIZE = "itemize"
    1.20 +  val ENUMERATE = "enumerate"
    1.21 +  val DESCRIPTION = "description"
    1.22  
    1.23  
    1.24    /* ML */