| author | blanchet |
| Fri, 27 Aug 2010 13:12:23 +0200 | |
| changeset 38823 | 828e68441a2f |
| parent 38568 | f117ba49a59c |
| child 38722 | ba31936497c2 |
| 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 |
|
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38355
diff
changeset
|
23 |
def get_range(pos: T): Option[Text.Range] = |
| 36677 | 24 |
(get_offset(pos), get_end_offset(pos)) match {
|
|
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38479
diff
changeset
|
25 |
case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop)) |
| 38568 | 26 |
case (Some(start), None) => Some(Text.Range(start)) |
|
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38479
diff
changeset
|
27 |
case (_, _) => None |
| 36677 | 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) }
|
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38355
diff
changeset
|
31 |
object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
|
| 27968 | 32 |
} |