src/Pure/PIDE/line.scala
changeset 64681 642b6105e6f4
parent 64679 b2bf280b7e13
child 64682 7e119f32276a
equal deleted inserted replaced
64680:7f87c1aa0ffa 64681:642b6105e6f4
    29       line compare that.line match {
    29       line compare that.line match {
    30         case 0 => column compare that.column
    30         case 0 => column compare that.column
    31         case i => i
    31         case i => i
    32       }
    32       }
    33 
    33 
    34     def advance(text: String, length: Length = Length): Position =
    34     def advance(text: String, text_length: Length): Position =
    35       if (text.isEmpty) this
    35       if (text.isEmpty) this
    36       else {
    36       else {
    37         val lines = Library.split_lines(text)
    37         val lines = Library.split_lines(text)
    38         val l = line + lines.length - 1
    38         val l = line + lines.length - 1
    39         val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last))
    39         val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last))
    40         Position(l, c)
    40         Position(l, c)
    41       }
    41       }
    42   }
    42   }
    43 
    43 
    44 
    44 
   105         case other: Document => lines == other.lines
   105         case other: Document => lines == other.lines
   106         case _ => false
   106         case _ => false
   107       }
   107       }
   108     override def hashCode(): Int = lines.hashCode
   108     override def hashCode(): Int = lines.hashCode
   109 
   109 
   110     def position(offset: Text.Offset, length: Length = Length): Position =
   110     def position(text_offset: Text.Offset, text_length: Length): Position =
   111     {
   111     {
   112       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
   112       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
   113       {
   113       {
   114         lines_rest match {
   114         lines_rest match {
   115           case Nil => require(i == 0); Position(lines_count)
   115           case Nil => require(i == 0); Position(lines_count)
   116           case line :: ls =>
   116           case line :: ls =>
   117             val n = line.text.length
   117             val n = line.text.length
   118             if (ls.isEmpty || i <= n)
   118             if (ls.isEmpty || i <= n)
   119               Position(lines_count).advance(line.text.substring(n - i), length)
   119               Position(lines_count).advance(line.text.substring(n - i), text_length)
   120             else move(i - (n + 1), lines_count + 1, ls)
   120             else move(i - (n + 1), lines_count + 1, ls)
   121         }
   121         }
   122       }
   122       }
   123       move(offset, 0, lines)
   123       move(text_offset, 0, lines)
   124     }
   124     }
   125 
   125 
   126     def range(text_range: Text.Range, length: Length = Length): Range =
   126     def range(text_range: Text.Range, text_length: Length): Range =
   127       Range(
   127       Range(
   128         position(text_range.start, length),
   128         position(text_range.start, text_length),
   129         position(text_range.stop, length))
   129         position(text_range.stop, text_length))
   130 
   130 
   131     def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
   131     def offset(pos: Position, text_length: Length): Option[Text.Offset] =
   132     {
   132     {
   133       val l = pos.line
   133       val l = pos.line
   134       val c = pos.column
   134       val c = pos.column
   135       if (0 <= l && l < lines.length) {
   135       if (0 <= l && l < lines.length) {
   136         val line_offset =
   136         val line_offset =
   137           if (l == 0) 0
   137           if (l == 0) 0
   138           else (0 /: lines.iterator.take(l - 1))({ case (n, line) => n + length(line.text) + 1 })
   138           else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 }
   139         length.offset(lines(l).text, c).map(line_offset + _)
   139         text_length.offset(lines(l).text, c).map(line_offset + _)
   140       }
   140       }
   141       else None
   141       else None
   142     }
   142     }
   143   }
   143   }
   144 
   144