author | wenzelm |
Tue, 02 Sep 2008 14:10:27 +0200 | |
changeset 28077 | d6102a4fcfce |
parent 27993 | 6dd90ef9f927 |
child 29140 | e7ac5bb20aed |
permissions | -rw-r--r-- |
27968 | 1 |
/* Title: Pure/General/position.scala |
2 |
ID: $Id$ |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Position properties. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
import java.util.Properties |
|
11 |
||
12 |
||
13 |
object Position { |
|
14 |
||
15 |
private def get_string(name: String, props: Properties) = { |
|
27989 | 16 |
val value = if (props != null) props.getProperty(name) else null |
27968 | 17 |
if (value != null) Some(value) else None |
18 |
} |
|
19 |
||
20 |
private def get_int(name: String, props: Properties) = { |
|
21 |
get_string(name, props) match { |
|
22 |
case None => None |
|
23 |
case Some(value) => |
|
24 |
try { Some(Integer.parseInt(value)) } |
|
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27989
diff
changeset
|
25 |
catch { case _: NumberFormatException => None } |
27968 | 26 |
} |
27 |
} |
|
28 |
||
29 |
def line_of(props: Properties) = get_int(Markup.LINE, props) |
|
30 |
def column_of(props: Properties) = get_int(Markup.COLUMN, props) |
|
31 |
def offset_of(props: Properties) = get_int(Markup.OFFSET, props) |
|
32 |
def end_line_of(props: Properties) = get_int(Markup.END_LINE, props) |
|
33 |
def end_column_of(props: Properties) = get_int(Markup.END_COLUMN, props) |
|
34 |
def end_offset_of(props: Properties) = get_int(Markup.END_OFFSET, props) |
|
35 |
def file_of(props: Properties) = get_string(Markup.FILE, props) |
|
36 |
def id_of(props: Properties) = get_string(Markup.ID, props) |
|
37 |
} |