7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Markup |
10 object Markup |
11 { |
11 { |
|
12 /* integers */ |
|
13 |
|
14 object Int { |
|
15 def apply(i: scala.Int): String = i.toString |
|
16 def unapply(s: String): Option[scala.Int] = |
|
17 try { Some(Integer.parseInt(s)) } |
|
18 catch { case _: NumberFormatException => None } |
|
19 } |
|
20 |
|
21 object Long { |
|
22 def apply(i: scala.Long): String = i.toString |
|
23 def unapply(s: String): Option[scala.Long] = |
|
24 try { Some(java.lang.Long.parseLong(s)) } |
|
25 catch { case _: NumberFormatException => None } |
|
26 } |
|
27 |
|
28 |
12 /* property values */ |
29 /* property values */ |
13 |
30 |
14 def get_string(name: String, props: List[(String, String)]): Option[String] = |
31 def get_string(name: String, props: List[(String, String)]): Option[String] = |
15 props.find(p => p._1 == name).map(_._2) |
32 props.find(p => p._1 == name).map(_._2) |
16 |
33 |
17 |
34 def get_long(name: String, props: List[(String, String)]): Option[scala.Long] = |
18 def parse_long(s: String): Option[Long] = |
|
19 try { Some(java.lang.Long.parseLong(s)) } |
|
20 catch { case _: NumberFormatException => None } |
|
21 |
|
22 def get_long(name: String, props: List[(String, String)]): Option[Long] = |
|
23 { |
35 { |
24 get_string(name, props) match { |
36 get_string(name, props) match { |
25 case None => None |
37 case None => None |
26 case Some(value) => parse_long(value) |
38 case Some(Long(i)) => Some(i) |
27 } |
39 } |
28 } |
40 } |
29 |
41 |
30 |
42 def get_int(name: String, props: List[(String, String)]): Option[scala.Int] = |
31 def parse_int(s: String): Option[Int] = |
|
32 try { Some(Integer.parseInt(s)) } |
|
33 catch { case _: NumberFormatException => None } |
|
34 |
|
35 def get_int(name: String, props: List[(String, String)]): Option[Int] = |
|
36 { |
43 { |
37 get_string(name, props) match { |
44 get_string(name, props) match { |
38 case None => None |
45 case None => None |
39 case Some(value) => parse_int(value) |
46 case Some(Int(i)) => Some(i) |
40 } |
47 } |
41 } |
48 } |
42 |
49 |
43 |
50 |
44 /* name */ |
51 /* name */ |