src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Tue Dec 20 10:06:18 2016 +0100
+++ b/src/Pure/General/symbol.scala	Tue Dec 20 10:44:36 2016 +0100
@@ -128,6 +128,9 @@
 
   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
 
+  def length(text: CharSequence): Int = iterator(text).length
+  object Length extends Line.Length { def apply(text: String): Int = length(text) }
+
 
   /* decoding offsets */