src/Pure/General/markup.scala
changeset 38355 8cb265fb12fe
parent 38259 2b61c5e27399
child 38414 49f1f657adc2
     1.1 --- a/src/Pure/General/markup.scala	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -14,6 +14,20 @@
     1.4    def get_string(name: String, props: List[(String, String)]): Option[String] =
     1.5      props.find(p => p._1 == name).map(_._2)
     1.6  
     1.7 +
     1.8 +  def parse_long(s: String): Option[Long] =
     1.9 +    try { Some(java.lang.Long.parseLong(s)) }
    1.10 +    catch { case _: NumberFormatException => None }
    1.11 +
    1.12 +  def get_long(name: String, props: List[(String, String)]): Option[Long] =
    1.13 +  {
    1.14 +    get_string(name, props) match {
    1.15 +      case None => None
    1.16 +      case Some(value) => parse_long(value)
    1.17 +    }
    1.18 +  }
    1.19 +
    1.20 +
    1.21    def parse_int(s: String): Option[Int] =
    1.22      try { Some(Integer.parseInt(s)) }
    1.23      catch { case _: NumberFormatException => None }