src/Tools/VSCode/src/line.scala
changeset 64610 1b89608974e9
parent 64605 9c1173a7e4cb
--- 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 {