src/Pure/PIDE/line.scala

tuned signature;

/*  Title:      Pure/PIDE/line.scala
    Author:     Makarius

Line-oriented text.
*/

package isabelle


import scala.annotation.tailrec


object Line
{
  /* position */

  object Position
  {
    val zero: Position = Position()
  }

  sealed case class Position(line: Int = 0, column: Int = 0)
  {
    def line1: Int = line + 1
    def column1: Int = column + 1
    def print: String = line1.toString + ":" + column1.toString

    def compare(that: Position): Int =
      line compare that.line match {
        case 0 => column compare that.column
        case i => i
      }

    def advance(text: String, length: Length = Length): Position =
      if (text.isEmpty) this
      else {
        val lines = Library.split_lines(text)
        val l = line + lines.length - 1
        val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last))
        Position(l, c)
      }
  }


  /* range (right-open interval) */

  object Range
  {
    val zero: Range = Range(Position.zero, Position.zero)
  }

  sealed case class Range(start: Position, stop: Position)
  {
    if (start.compare(stop) > 0)
      error("Bad line range: " + start.print + ".." + stop.print)

    def print: String =
      if (start == stop) start.print