author | wenzelm |
Wed, 11 Aug 2010 22:41:26 +0200 | |
changeset 38355 | 8cb265fb12fe |
parent 36683 | 41a1210519fd |
child 38479 | e628da370072 |
permissions | -rw-r--r-- |
27968 | 1 |
/* Title: Pure/General/position.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Position properties. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
32450 | 10 |
object Position |
11 |
{ |
|
31705 | 12 |
type T = List[(String, String)] |
27968 | 13 |
|
36683 | 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) |
|
38355
8cb265fb12fe
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);
wenzelm
parents:
36683
diff
changeset
|
21 |
def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos) |
31705 | 22 |
|
36677 | 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 |
||
38355
8cb265fb12fe
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);
wenzelm
parents:
36683
diff
changeset
|
30 |
object Id { def unapply(pos: T): Option[Long] = get_id(pos) } |
36677 | 31 |
object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) } |
27968 | 32 |
} |