| author | wenzelm |
| Fri, 19 Dec 2008 20:37:29 +0100 | |
| changeset 29140 | e7ac5bb20aed |
| parent 27993 | 6dd90ef9f927 |
| child 31705 | 0c83e3e75fcf |
| 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 |
import java.util.Properties |
|
10 |
||
11 |
||
12 |
object Position {
|
|
13 |
||
14 |
private def get_string(name: String, props: Properties) = {
|
|
| 27989 | 15 |
val value = if (props != null) props.getProperty(name) else null |
| 27968 | 16 |
if (value != null) Some(value) else None |
17 |
} |
|
18 |
||
19 |
private def get_int(name: String, props: Properties) = {
|
|
20 |
get_string(name, props) match {
|
|
21 |
case None => None |
|
22 |
case Some(value) => |
|
23 |
try { Some(Integer.parseInt(value)) }
|
|
|
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27989
diff
changeset
|
24 |
catch { case _: NumberFormatException => None }
|
| 27968 | 25 |
} |
26 |
} |
|
27 |
||
28 |
def line_of(props: Properties) = get_int(Markup.LINE, props) |
|
29 |
def column_of(props: Properties) = get_int(Markup.COLUMN, props) |
|
30 |
def offset_of(props: Properties) = get_int(Markup.OFFSET, props) |
|
31 |
def end_line_of(props: Properties) = get_int(Markup.END_LINE, props) |
|
32 |
def end_column_of(props: Properties) = get_int(Markup.END_COLUMN, props) |
|
33 |
def end_offset_of(props: Properties) = get_int(Markup.END_OFFSET, props) |
|
34 |
def file_of(props: Properties) = get_string(Markup.FILE, props) |
|
35 |
def id_of(props: Properties) = get_string(Markup.ID, props) |
|
36 |
} |