| changeset 74683 | c8327efc7af1 |
| parent 73528 | c337c798f64c |
| child 74731 | 161e84e6b40a |
--- 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 */