# HG changeset patch
# User wenzelm
# Date 1648756088 -7200
# Node ID 4f6a6ba7387df4b80c59248343dc08767f5908f0
# Parent  14154ac511ba76b271f0896ceda00e047a2736b4
tuned: avoid problems with scala3;

diff -r 14154ac511ba -r 4f6a6ba7387d src/Pure/Thy/presentation.scala
--- 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