# HG changeset patch
# User wenzelm
# Date 1636025123 -3600
# Node ID c8327efc7af1da4cf93cd33830192a55cea45fc7
# Parent  ce4adcc85f6c2aec9901309a26e876c3f52a2f2d
clarified signature: more direct XML.symbol_length;

diff -r ce4adcc85f6c -r c8327efc7af1 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Nov 04 12:19:49 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Thu Nov 04 12:25:23 2021 +0100
@@ -109,6 +109,7 @@
   }
 
   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
+  def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
 
 
   /* text content */
diff -r ce4adcc85f6c -r c8327efc7af1 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Nov 04 12:19:49 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 04 12:25:23 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(XML.content(text)))
+          (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)
@@ -177,7 +177,7 @@
           }
       }
 
-    html_body(xml, Symbol.length(XML.content(xml)) + 1)._1
+    html_body(xml, XML.symbol_length(xml) + 1)._1
   }