src/Pure/General/value.scala
author wenzelm
Tue Dec 11 23:59:41 2018 +0100 (8 months ago)
changeset 69450 b28b001e7ee8
parent 68946 6dd1460f6920
child 69452 704915cf59fa
permissions -rw-r--r--
more operations (as in ML);
     1 /*  Title:      Pure/General/value.scala
     2     Author:     Makarius
     3 
     4 Plain values, represented as string.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Value
    11 {
    12   object Boolean
    13   {
    14     def apply(x: scala.Boolean): java.lang.String = x.toString
    15     def unapply(s: java.lang.String): Option[scala.Boolean] =
    16       s match {
    17         case "true" => Some(true)
    18         case "false" => Some(false)
    19         case _ => None
    20       }
    21     def parse(s: java.lang.String): scala.Boolean =
    22       unapply(s) getOrElse error("Bad boolean: " + quote(s))
    23   }
    24 
    25   object Int
    26   {
    27     def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
    28     def unapply(s: java.lang.String): Option[scala.Int] =
    29       try { Some(Integer.parseInt(s)) }
    30       catch { case _: NumberFormatException => None }
    31     def parse(s: java.lang.String): scala.Int =
    32       unapply(s) getOrElse error("Bad integer: " + quote(s))
    33 
    34     def parse_nat(s: java.lang.String): scala.Int =
    35       s match {
    36         case Value.Int(n) if n >= 0 => n
    37         case _ => error("Bad natural number: " + quote(s))
    38       }
    39   }
    40 
    41   object Long
    42   {
    43     def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
    44     def unapply(s: java.lang.String): Option[scala.Long] =
    45       try { Some(java.lang.Long.parseLong(s)) }
    46       catch { case _: NumberFormatException => None }
    47     def parse(s: java.lang.String): scala.Long =
    48       unapply(s) getOrElse error("Bad integer: " + quote(s))
    49   }
    50 
    51   object Double
    52   {
    53     def apply(x: scala.Double): java.lang.String = x.toString
    54     def unapply(s: java.lang.String): Option[scala.Double] =
    55       try { Some(java.lang.Double.parseDouble(s)) }
    56       catch { case _: NumberFormatException => None }
    57     def parse(s: java.lang.String): scala.Double =
    58       unapply(s) getOrElse error("Bad real: " + quote(s))
    59   }
    60 
    61   object Seconds
    62   {
    63     def apply(t: Time): java.lang.String =
    64     {
    65       val s = t.seconds
    66       if (s.toInt.toDouble == s) s.toInt.toString else t.toString
    67     }
    68     def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
    69     def parse(s: java.lang.String): Time =
    70       unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
    71   }
    72 }