src/Pure/PIDE/line.scala
changeset 64614 88211daacf93
parent 64611 d72d63d05bdb
child 64615 fd0d6de380c6
equal deleted inserted replaced
64613:d1ca9ce0d9e4 64614:88211daacf93
    41       Position(l, c)
    41       Position(l, c)
    42     }
    42     }
    43 
    43 
    44     def advance(text: String): Position =
    44     def advance(text: String): Position =
    45       if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
    45       if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
    46 
       
    47     def advance_symbols(text: String): Position =
       
    48       if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
       
    49 
    46 
    50     def advance_codepoints(text: String): Position =
    47     def advance_codepoints(text: String): Position =
    51       if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
    48       if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
    52   }
    49   }
    53 
    50 
   105       }
   102       }
   106       move(offset, 0, lines)
   103       move(offset, 0, lines)
   107     }
   104     }
   108 
   105 
   109     def position(i: Text.Offset): Position = position(_.advance(_), i)
   106     def position(i: Text.Offset): Position = position(_.advance(_), i)
   110     def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i)
       
   111     def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
   107     def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
   112 
   108 
   113     // FIXME symbols, codepoints
   109     // FIXME codepoints
   114     def offset(pos: Position): Option[Text.Offset] =
   110     def offset(pos: Position): Option[Text.Offset] =
   115     {
   111     {
   116       val l = pos.line
   112       val l = pos.line
   117       val c = pos.column
   113       val c = pos.column
   118       if (0 <= l && l < lines.length) {
   114       if (0 <= l && l < lines.length) {
   134 
   130 
   135 final class Line private(val text: String)
   131 final class Line private(val text: String)
   136 {
   132 {
   137   require(text.forall(c => c != '\r' && c != '\n'))
   133   require(text.forall(c => c != '\r' && c != '\n'))
   138 
   134 
   139   lazy val length_symbols: Int = Symbol.iterator(text).length
       
   140   lazy val length_codepoints: Int = Codepoint.iterator(text).length
   135   lazy val length_codepoints: Int = Codepoint.iterator(text).length
   141 
   136 
   142   override def equals(that: Any): Boolean =
   137   override def equals(that: Any): Boolean =
   143     that match {
   138     that match {
   144       case other: Line => text == other.text
   139       case other: Line => text == other.text