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;
     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[Text.Range] =
    24     (get_offset(pos), get_end_offset(pos)) match {
    25       case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
    26       case (Some(start), None) => Some(Text.Range(start, start))
    27       case (_, _) => None
    28     }
    29 
    30   object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
    31   object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
    32 }