src/Pure/Thy/presentation.scala
changeset 75379 4f6a6ba7387d
parent 74841 9ad3fa47c83e
child 75393 87ebf5a50283
--- a/src/Pure/Thy/presentation.scala	Wed Mar 30 16:18:25 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Thu Mar 31 21:48:08 2022 +0200
@@ -210,7 +210,7 @@
   /* HTML output */
 
   private val div_elements =
-    Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
+    Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.`enum`.name,
       HTML.descr.name)
 
   def make_html(
@@ -261,7 +261,7 @@
           (Nil, end_offset - XML.symbol_length(text))
         case XML.Elem(Markup.Markdown_List(kind), body) =>
           val (body1, offset) = html_body(body, end_offset)
-          if (kind == Markup.ENUMERATE) (List(HTML.enum(body1)), offset)
+          if (kind == Markup.ENUMERATE) (List(HTML.`enum`(body1)), offset)
           else (List(HTML.list(body1)), offset)
         case XML.Elem(markup, body) =>
           val name = markup.name