src/Pure/PIDE/line.scala
changeset 64617 01e50039edc9
parent 64615 fd0d6de380c6
child 64619 e3d9a31281f3
equal deleted inserted replaced
64616:dc3ec40fe41b 64617:01e50039edc9
    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 
       
    21   /* position */
    15   /* position */
    22 
    16 
    23   object Position
    17   object Position
    24   {
    18   {
    25     val zero: Position = Position(0, 0)
    19     val zero: Position = Position(0, 0)
    35       line compare that.line match {
    29       line compare that.line match {
    36         case 0 => column compare that.column
    30         case 0 => column compare that.column
    37         case i => i
    31         case i => i
    38       }
    32       }
    39 
    33 
    40     private def advance[A](iterator: Iterator[A], is_newline: A => Boolean): Position =
    34     def advance(text: String, length: Length = Length): Position =
    41     {
    35       if (text.isEmpty) this
    42       var l = line
    36       else {
    43       var c = column
    37         val lines = Library.split_lines(text)
    44       for (x <- iterator) {
    38         Position(line + lines.length - 1, column + length(Library.trim_line(lines.last)))
    45         if (is_newline(x)) { l += 1; c = 0 } else c += 1
       
    46       }
    39       }
    47       Position(l, c)
       
    48     }
       
    49 
       
    50     def advance(text: String): Position =
       
    51       if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
       
    52 
       
    53     def advance_codepoints(text: String): Position =
       
    54       if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
       
    55   }
    40   }
    56 
    41 
    57 
    42 
    58   /* range (right-open interval) */
    43   /* range (right-open interval) */
    59 
    44 
    92         case other: Document => lines == other.lines
    77         case other: Document => lines == other.lines
    93         case _ => false
    78         case _ => false
    94       }
    79       }
    95     override def hashCode(): Int = lines.hashCode
    80     override def hashCode(): Int = lines.hashCode
    96 
    81 
    97     private def position(advance: (Position, String) => Position, offset: Text.Offset): Position =
    82     def position(offset: Text.Offset, length: Length = Length): Position =
    98     {
    83     {
    99       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
    84       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
   100       {
    85       {
   101         lines_rest match {
    86         lines_rest match {
   102           case Nil => require(i == 0); Position(lines_count, 0)
    87           case Nil => require(i == 0); Position(lines_count, 0)
   103           case line :: ls =>
    88           case line :: ls =>
   104             val n = line.text.length
    89             val n = line.text.length
   105             if (ls.isEmpty || i <= n) advance(Position(lines_count, 0), line.text.substring(n - i))
    90             if (ls.isEmpty || i <= n)
       
    91               Position(lines_count, 0).advance(line.text.substring(n - i), length)
   106             else move(i - (n + 1), lines_count + 1, ls)
    92             else move(i - (n + 1), lines_count + 1, ls)
   107         }
    93         }
   108       }
    94       }
   109       move(offset, 0, lines)
    95       move(offset, 0, lines)
   110     }
    96     }
   111 
    97 
   112     def position(i: Text.Offset): Position = position(_.advance(_), i)
    98     def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
   113     def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
       
   114 
       
   115     // FIXME codepoints
       
   116     def offset(pos: Position): Option[Text.Offset] =
       
   117     {
    99     {
   118       val l = pos.line
   100       val l = pos.line
   119       val c = pos.column
   101       val c = pos.column
   120       if (0 <= l && l < lines.length) {
   102       if (0 <= l && l < lines.length) {
   121         val line_offset =
   103         val line_offset =
   122           if (l == 0) 0
   104           if (l == 0) 0
   123           else (0 /: lines.take(l - 1))({ case (n, line) => n + line.text.length + 1 })
   105           else (0 /: lines.iterator.take(l - 1))({ case (n, line) => n + length(line.text) + 1 })
   124         if (c <= lines(l).text.length) Some(line_offset + c) else None
   106         length.offset(lines(l).text, c).map(line_offset + _)
   125       }
   107       }
   126       else None
   108       else None
   127     }
   109     }
   128   }
   110   }
   129 
   111