src/Pure/General/position.scala
author wenzelm
Wed Aug 11 22:41:26 2010 +0200 (2010-08-11)
changeset 38355 8cb265fb12fe
parent 36683 41a1210519fd
child 38479 e628da370072
permissions -rw-r--r--
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
     1 /*  Title:      Pure/General/position.scala
     2     Author:     Makarius
     3 
     4 Position properties.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Position
    11 {
    12   type T = List[(String, String)]
    13 
    14   def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
    15   def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
    16   def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
    17   def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
    18   def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
    19   def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
    20   def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
    21   def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
    22 
    23   def get_range(pos: T): Option[(Int, Int)] =
    24     (get_offset(pos), get_end_offset(pos)) match {
    25       case (Some(begin), Some(end)) => Some(begin, end)
    26       case (Some(begin), None) => Some(begin, begin + 1)
    27       case (None, _) => None
    28     }
    29 
    30   object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
    31   object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
    32 }