src/Pure/PIDE/line.scala
changeset 64689 f32efd2eeb2c
parent 64688 d8f194556c70
child 64701 931f51fb24ca
--- a/src/Pure/PIDE/line.scala	Wed Dec 28 19:15:52 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 19:16:45 2016 +0100
@@ -150,8 +150,6 @@
 {
   require(text.forall(c => c != '\r' && c != '\n'))
 
-  lazy val length_codepoints: Int = Codepoint.iterator(text).length
-
   override def equals(that: Any): Boolean =
     that match {
       case other: Line => text == other.text