src/Pure/PIDE/markup.scala
changeset 67322 734a4e44b159
parent 66942 91a21a5631ae
child 67323 d02208cefbdb
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Jan 02 13:16:32 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Jan 02 15:38:22 2018 +0100
     1.3 @@ -297,7 +297,7 @@
     1.4  
     1.5    val MARKDOWN_PARAGRAPH = "markdown_paragraph"
     1.6    val Markdown_List = new Markup_String("markdown_list", "kind")
     1.7 -  val Markdown_Item = new Markup_Int("markdown_item", "depth")
     1.8 +  val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
     1.9  
    1.10  
    1.11    /* ML */