author | wenzelm |
Wed, 30 Dec 2009 20:25:35 +0100 | |
changeset 34211 | 686f828548ef |
parent 32450 | 375db037f4d2 |
child 36677 | 1225dd15827d |
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 |
|
31705 | 14 |
private def get_string(name: String, pos: T): Option[String] = |
15 |
pos.find(p => p._1 == name).map(_._2) |
|
16 |
||
17 |
private def get_int(name: String, pos: T): Option[Int] = |
|
18 |
{ |
|
19 |
get_string(name, pos) match { |
|
27968 | 20 |
case None => None |
21 |
case Some(value) => |
|
22 |
try { Some(Integer.parseInt(value)) } |
|
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27989
diff
changeset
|
23 |
catch { case _: NumberFormatException => None } |
27968 | 24 |
} |
25 |
} |
|
26 |
||
34211 | 27 |
def get_line(pos: T): Option[Int] = get_int(Markup.LINE, pos) |
28 |
def get_column(pos: T): Option[Int] = get_int(Markup.COLUMN, pos) |
|
29 |
def get_offset(pos: T): Option[Int] = get_int(Markup.OFFSET, pos) |
|
30 |
def get_end_line(pos: T): Option[Int] = get_int(Markup.END_LINE, pos) |
|
31 |
def get_end_column(pos: T): Option[Int] = get_int(Markup.END_COLUMN, pos) |
|
32 |
def get_end_offset(pos: T): Option[Int] = get_int(Markup.END_OFFSET, pos) |
|
33 |
def get_file(pos: T): Option[String] = get_string(Markup.FILE, pos) |
|
34 |
def get_id(pos: T): Option[String] = get_string(Markup.ID, pos) |
|
31705 | 35 |
|
34211 | 36 |
def get_offsets(pos: T): (Option[Int], Option[Int]) = |
31705 | 37 |
{ |
34211 | 38 |
val begin = get_offset(pos) |
39 |
val end = get_end_offset(pos) |
|
31705 | 40 |
(begin, if (end.isDefined) end else begin.map(_ + 1)) |
41 |
} |
|
27968 | 42 |
} |