| changeset 67323 | d02208cefbdb |
| parent 67322 | 734a4e44b159 |
| child 67336 | 3ee6da378183 |
--- a/src/Pure/PIDE/markup.scala Tue Jan 02 15:38:22 2018 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Jan 02 19:52:17 2018 +0100 @@ -296,6 +296,7 @@ /* Markdown document structure */ val MARKDOWN_PARAGRAPH = "markdown_paragraph" + val MARKDOWN_ITEM = "markdown_item" val Markdown_List = new Markup_String("markdown_list", "kind") val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")