src/Pure/General/value.scala
author wenzelm
Sat Sep 08 13:22:23 2018 +0200 (10 months ago)
changeset 68946 6dd1460f6920
parent 68944 ce68b1488612
child 69450 b28b001e7ee8
permissions -rw-r--r--
more accurate output;
     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 
    35   object Long
    36   {
    37     def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
    38     def unapply(s: java.lang.String): Option[scala.Long] =
    39       try { Some(java.lang.Long.parseLong(s)) }
    40       catch { case _: NumberFormatException => None }
    41     def parse(s: java.lang.String): scala.Long =
    42       unapply(s) getOrElse error("Bad integer: " + quote(s))
    43   }
    44 
    45   object Double
    46   {
    47     def apply(x: scala.Double): java.lang.String = x.toString
    48     def unapply(s: java.lang.String): Option[scala.Double] =
    49       try { Some(java.lang.Double.parseDouble(s)) }
    50       catch { case _: NumberFormatException => None }
    51     def parse(s: java.lang.String): scala.Double =
    52       unapply(s) getOrElse error("Bad real: " + quote(s))
    53   }
    54 
    55   object Seconds
    56   {
    57     def apply(t: Time): java.lang.String =
    58     {
    59       val s = t.seconds
    60       if (s.toInt.toDouble == s) s.toInt.toString else t.toString
    61     }
    62     def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
    63     def parse(s: java.lang.String): Time =
    64       unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
    65   }
    66 }