src/Pure/PIDE/line.scala
changeset 64615 fd0d6de380c6
parent 64614 88211daacf93
child 64617 01e50039edc9
equal deleted inserted replaced
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)