20 } |
18 } |
21 def parse(s: java.lang.String): scala.Boolean = |
19 def parse(s: java.lang.String): scala.Boolean = |
22 unapply(s) getOrElse error("Bad boolean: " + quote(s)) |
20 unapply(s) getOrElse error("Bad boolean: " + quote(s)) |
23 } |
21 } |
24 |
22 |
25 object Nat |
23 object Nat { |
26 { |
|
27 def unapply(s: java.lang.String): Option[scala.Int] = |
24 def unapply(s: java.lang.String): Option[scala.Int] = |
28 s match { |
25 s match { |
29 case Int(n) if n >= 0 => Some(n) |
26 case Int(n) if n >= 0 => Some(n) |
30 case _ => None |
27 case _ => None |
31 } |
28 } |
32 def parse(s: java.lang.String): scala.Int = |
29 def parse(s: java.lang.String): scala.Int = |
33 unapply(s) getOrElse error("Bad natural number: " + quote(s)) |
30 unapply(s) getOrElse error("Bad natural number: " + quote(s)) |
34 } |
31 } |
35 |
32 |
36 object Int |
33 object Int { |
37 { |
|
38 def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x) |
34 def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x) |
39 def unapply(s: java.lang.String): Option[scala.Int] = |
35 def unapply(s: java.lang.String): Option[scala.Int] = |
40 try { Some(Integer.parseInt(s)) } |
36 try { Some(Integer.parseInt(s)) } |
41 catch { case _: NumberFormatException => None } |
37 catch { case _: NumberFormatException => None } |
42 def parse(s: java.lang.String): scala.Int = |
38 def parse(s: java.lang.String): scala.Int = |
43 unapply(s) getOrElse error("Bad integer: " + quote(s)) |
39 unapply(s) getOrElse error("Bad integer: " + quote(s)) |
44 } |
40 } |
45 |
41 |
46 object Long |
42 object Long { |
47 { |
|
48 def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x) |
43 def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x) |
49 def unapply(s: java.lang.String): Option[scala.Long] = |
44 def unapply(s: java.lang.String): Option[scala.Long] = |
50 try { Some(java.lang.Long.parseLong(s)) } |
45 try { Some(java.lang.Long.parseLong(s)) } |
51 catch { case _: NumberFormatException => None } |
46 catch { case _: NumberFormatException => None } |
52 def parse(s: java.lang.String): scala.Long = |
47 def parse(s: java.lang.String): scala.Long = |
53 unapply(s) getOrElse error("Bad integer: " + quote(s)) |
48 unapply(s) getOrElse error("Bad integer: " + quote(s)) |
54 } |
49 } |
55 |
50 |
56 object Double |
51 object Double { |
57 { |
|
58 def apply(x: scala.Double): java.lang.String = x.toString |
52 def apply(x: scala.Double): java.lang.String = x.toString |
59 def unapply(s: java.lang.String): Option[scala.Double] = |
53 def unapply(s: java.lang.String): Option[scala.Double] = |
60 try { Some(java.lang.Double.parseDouble(s)) } |
54 try { Some(java.lang.Double.parseDouble(s)) } |
61 catch { case _: NumberFormatException => None } |
55 catch { case _: NumberFormatException => None } |
62 def parse(s: java.lang.String): scala.Double = |
56 def parse(s: java.lang.String): scala.Double = |
63 unapply(s) getOrElse error("Bad real: " + quote(s)) |
57 unapply(s) getOrElse error("Bad real: " + quote(s)) |
64 } |
58 } |
65 |
59 |
66 object Seconds |
60 object Seconds { |
67 { |
61 def apply(t: Time): java.lang.String = { |
68 def apply(t: Time): java.lang.String = |
|
69 { |
|
70 val s = t.seconds |
62 val s = t.seconds |
71 if (s.toInt.toDouble == s) s.toInt.toString else t.toString |
63 if (s.toInt.toDouble == s) s.toInt.toString else t.toString |
72 } |
64 } |
73 def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds) |
65 def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds) |
74 def parse(s: java.lang.String): Time = |
66 def parse(s: java.lang.String): Time = |