# HG changeset patch
# User wenzelm
# Date 1636024789 -3600
# Node ID ce4adcc85f6c2aec9901309a26e876c3f52a2f2d
# Parent  84e5b4339db6384e9e7c5cb24e1bd57833482bc5
more direct Symbol.length: Symbol.decode is redundant, symbol counts are invariant under it;

diff -r 84e5b4339db6 -r ce4adcc85f6c src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Nov 04 12:01:28 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 04 12:19:49 2021 +0100
@@ -149,7 +149,7 @@
           val (body1, offset) = html_body(body, end_offset)
           (List(HTML.item(body1)), offset)
         case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), text) =>
-          (Nil, end_offset - Symbol.length(Symbol.decode(XML.content(text))))
+          (Nil, end_offset - Symbol.length(XML.content(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)
@@ -169,16 +169,15 @@
             case None => (html_class(name, html), offset)
           }
         case XML.Text(text) =>
-          val decoded = Symbol.decode(text)
-          val offset = end_offset - Symbol.length(decoded)
-          val body = HTML.text(decoded)
+          val offset = end_offset - Symbol.length(text)
+          val body = HTML.text(Symbol.decode(text))
           entity_anchor(context, Text.Range(offset, end_offset), body) match {
             case Some(body1) => (List(body1), offset)
             case None => (body, offset)
           }
       }
 
-    html_body(xml, Symbol.length(Symbol.decode(XML.content(xml))) + 1)._1
+    html_body(xml, Symbol.length(XML.content(xml)) + 1)._1
   }