src/Pure/General/position.scala
author wenzelm
Fri Aug 20 11:00:15 2010 +0200 (2010-08-20)
changeset 38565 32b924a832c4
parent 38479 e628da370072
child 38568 f117ba49a59c
permissions -rw-r--r--
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm@27968
     1
/*  Title:      Pure/General/position.scala
wenzelm@27968
     2
    Author:     Makarius
wenzelm@27968
     3
wenzelm@27968
     4
Position properties.
wenzelm@27968
     5
*/
wenzelm@27968
     6
wenzelm@27968
     7
package isabelle
wenzelm@27968
     8
wenzelm@27968
     9
wenzelm@32450
    10
object Position
wenzelm@32450
    11
{
wenzelm@31705
    12
  type T = List[(String, String)]
wenzelm@27968
    13
wenzelm@36683
    14
  def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
wenzelm@36683
    15
  def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
wenzelm@36683
    16
  def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
wenzelm@36683
    17
  def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
wenzelm@36683
    18
  def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
wenzelm@36683
    19
  def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
wenzelm@36683
    20
  def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
wenzelm@38355
    21
  def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
wenzelm@31705
    22
wenzelm@38479
    23
  def get_range(pos: T): Option[Text.Range] =
wenzelm@36677
    24
    (get_offset(pos), get_end_offset(pos)) match {
wenzelm@38565
    25
      case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
wenzelm@38565
    26
      case (Some(start), None) => Some(Text.Range(start, start))
wenzelm@38565
    27
      case (_, _) => None
wenzelm@36677
    28
    }
wenzelm@36677
    29
wenzelm@38355
    30
  object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
wenzelm@38479
    31
  object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
wenzelm@27968
    32
}