wenzelm@27968: /*  Title:      Pure/General/position.scala
wenzelm@27968:     Author:     Makarius
wenzelm@27968: 
wenzelm@27968: Position properties.
wenzelm@27968: */
wenzelm@27968: 
wenzelm@27968: package isabelle
wenzelm@27968: 
wenzelm@27968: 
wenzelm@32450: object Position
wenzelm@32450: {
wenzelm@31705:   type T = List[(String, String)]
wenzelm@27968: 
wenzelm@36683:   def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
wenzelm@36683:   def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
wenzelm@36683:   def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
wenzelm@36683:   def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
wenzelm@36683:   def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
wenzelm@36683:   def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
wenzelm@36683:   def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
wenzelm@38355:   def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
wenzelm@31705: 
wenzelm@38479:   def get_range(pos: T): Option[Text.Range] =
wenzelm@36677:     (get_offset(pos), get_end_offset(pos)) match {
wenzelm@38565:       case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
wenzelm@38565:       case (Some(start), None) => Some(Text.Range(start, start))
wenzelm@38565:       case (_, _) => None
wenzelm@36677:     }
wenzelm@36677: 
wenzelm@38355:   object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
wenzelm@38479:   object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
wenzelm@27968: }