equal
deleted
inserted
replaced
22 c |
22 c |
23 } |
23 } |
24 } |
24 } |
25 |
25 |
26 def length(s: String): Int = iterator(s).length |
26 def length(s: String): Int = iterator(s).length |
27 |
|
28 trait Length extends Text.Length |
|
29 { |
|
30 protected def codepoint_length(c: Int): Int = 1 |
|
31 |
|
32 def apply(s: String): Int = |
|
33 (0 /: iterator(s)) { case (n, c) => n + codepoint_length(c) } |
|
34 |
|
35 def offset(s: String, i: Int): Option[Text.Offset] = |
|
36 { |
|
37 if (i <= 0 || s.forall(_ < 0x80)) Text.Length.offset(s, i) |
|
38 else { |
|
39 val length = s.length |
|
40 var offset = 0 |
|
41 var j = 0 |
|
42 while (offset < length && j < i) { |
|
43 val c = s.codePointAt(offset) |
|
44 offset += Character.charCount(c) |
|
45 j += codepoint_length(c) |
|
46 } |
|
47 if (j >= i) Some(offset) else None |
|
48 } |
|
49 } |
|
50 } |
|
51 |
|
52 object Length extends Length |
|
53 } |
27 } |