changeset 69450 | b28b001e7ee8 |
parent 68946 | 6dd1460f6920 |
child 69452 | 704915cf59fa |
--- a/src/Pure/General/value.scala Tue Dec 11 21:23:02 2018 +0100 +++ b/src/Pure/General/value.scala Tue Dec 11 23:59:41 2018 +0100 @@ -30,6 +30,12 @@ catch { case _: NumberFormatException => None } def parse(s: java.lang.String): scala.Int = unapply(s) getOrElse error("Bad integer: " + quote(s)) + + def parse_nat(s: java.lang.String): scala.Int = + s match { + case Value.Int(n) if n >= 0 => n + case _ => error("Bad natural number: " + quote(s)) + } } object Long