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