changeset 64615 | fd0d6de380c6 |
parent 64614 | 88211daacf93 |
child 64617 | 01e50039edc9 |
--- a/src/Pure/PIDE/line.scala Tue Dec 20 10:06:18 2016 +0100 +++ b/src/Pure/PIDE/line.scala Tue Dec 20 10:44:36 2016 +0100 @@ -12,6 +12,12 @@ object Line { + /* length wrt. encoding */ + + trait Length { def apply(text: String): Int } + object Length extends Length { def apply(text: String): Int = text.length } + + /* position */ object Position