src/Pure/PIDE/markup.scala
changeset 67323 d02208cefbdb
parent 67322 734a4e44b159
child 67336 3ee6da378183
equal deleted inserted replaced
67322:734a4e44b159 67323:d02208cefbdb
   294 
   294 
   295 
   295 
   296   /* Markdown document structure */
   296   /* Markdown document structure */
   297 
   297 
   298   val MARKDOWN_PARAGRAPH = "markdown_paragraph"
   298   val MARKDOWN_PARAGRAPH = "markdown_paragraph"
       
   299   val MARKDOWN_ITEM = "markdown_item"
   299   val Markdown_List = new Markup_String("markdown_list", "kind")
   300   val Markdown_List = new Markup_String("markdown_list", "kind")
   300   val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
   301   val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
   301 
   302 
   302 
   303 
   303   /* ML */
   304   /* ML */