--- a/src/Tools/VSCode/src/line.scala Tue Dec 20 08:46:38 2016 +0100
+++ b/src/Tools/VSCode/src/line.scala Tue Dec 20 08:53:26 2016 +0100
@@ -50,7 +50,7 @@
if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
def advance_codepoints(text: String): Position =
- if (text.isEmpty) this else advance[Int](Word.codepoint_iterator(text), _ == 10)
+ if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
}
@@ -139,7 +139,7 @@
require(text.forall(c => c != '\r' && c != '\n'))
lazy val length_symbols: Int = Symbol.iterator(text).length
- lazy val length_codepoints: Int = Word.codepoint_iterator(text).length
+ lazy val length_codepoints: Int = Codepoint.iterator(text).length
override def equals(that: Any): Boolean =
that match {