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