src/Pure/Isar/token.scala

--- a/src/Pure/Isar/token.scala	Fri Nov 20 14:29:21 2020 +0100
+++ b/src/Pure/Isar/token.scala	Fri Nov 20 23:47:34 2020 +0100
@@ -328,6 +328,8 @@
   def is_end: Boolean = is_command("end")
   def is_begin_or_command: Boolean = is_begin || is_command
 
+  def symbol_length: Symbol.Offset = Symbol.iterator(source).length
+
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
     else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source)