src/Pure/PIDE/line.scala

--- a/src/Pure/PIDE/line.scala	Tue Dec 20 10:06:18 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Tue Dec 20 10:44:36 2016 +0100
@@ -12,6 +12,12 @@
 
 object Line
 {
+  /* length wrt. encoding */
+
+  trait Length { def apply(text: String): Int }
+  object Length extends Length { def apply(text: String): Int = text.length }
+
+
   /* position */
 
   object Position