changeset 64615 | fd0d6de380c6 |
parent 64614 | 88211daacf93 |
child 64617 | 01e50039edc9 |
64614:88211daacf93 | 64615:fd0d6de380c6 |
---|---|
10 import scala.annotation.tailrec |
10 import scala.annotation.tailrec |
11 |
11 |
12 |
12 |
13 object Line |
13 object Line |
14 { |
14 { |
15 /* length wrt. encoding */ |
|
16 |
|
17 trait Length { def apply(text: String): Int } |
|
18 object Length extends Length { def apply(text: String): Int = text.length } |
|
19 |
|
20 |
|
15 /* position */ |
21 /* position */ |
16 |
22 |
17 object Position |
23 object Position |
18 { |
24 { |
19 val zero: Position = Position(0, 0) |
25 val zero: Position = Position(0, 0) |