src/Tools/jEdit/src/jedit_rendering.scala
changeset 67323 d02208cefbdb
parent 66150 c2e19b9e1398
child 67365 fb539f83683a
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 02 15:38:22 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 02 19:52:17 2018 +0100
@@ -120,7 +120,7 @@
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
-      Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
+      Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
 
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION,