src/Pure/General/properties.scala
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 43780 2cb2310d68b6
child 45667 546d78f0d81f
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm@43780
     1
/*  Title:      Pure/General/properties.scala
wenzelm@43780
     2
    Author:     Makarius
wenzelm@43780
     3
wenzelm@43780
     4
Property lists.
wenzelm@43780
     5
*/
wenzelm@43780
     6
wenzelm@43780
     7
package isabelle
wenzelm@43780
     8
wenzelm@43780
     9
wenzelm@43780
    10
object Properties
wenzelm@43780
    11
{
wenzelm@43780
    12
  /* plain values */
wenzelm@43780
    13
wenzelm@43780
    14
  object Value
wenzelm@43780
    15
  {
wenzelm@43780
    16
    object Int
wenzelm@43780
    17
    {
wenzelm@43780
    18
      def apply(x: scala.Int): java.lang.String = x.toString
wenzelm@43780
    19
      def unapply(s: java.lang.String): Option[scala.Int] =
wenzelm@43780
    20
        try { Some(Integer.parseInt(s)) }
wenzelm@43780
    21
        catch { case _: NumberFormatException => None }
wenzelm@43780
    22
    }
wenzelm@43780
    23
wenzelm@43780
    24
    object Long
wenzelm@43780
    25
    {
wenzelm@43780
    26
      def apply(x: scala.Long): java.lang.String = x.toString
wenzelm@43780
    27
      def unapply(s: java.lang.String): Option[scala.Long] =
wenzelm@43780
    28
        try { Some(java.lang.Long.parseLong(s)) }
wenzelm@43780
    29
        catch { case _: NumberFormatException => None }
wenzelm@43780
    30
    }
wenzelm@43780
    31
wenzelm@43780
    32
    object Double
wenzelm@43780
    33
    {
wenzelm@43780
    34
      def apply(x: scala.Double): java.lang.String = x.toString
wenzelm@43780
    35
      def unapply(s: java.lang.String): Option[scala.Double] =
wenzelm@43780
    36
        try { Some(java.lang.Double.parseDouble(s)) }
wenzelm@43780
    37
        catch { case _: NumberFormatException => None }
wenzelm@43780
    38
    }
wenzelm@43780
    39
  }
wenzelm@43780
    40
wenzelm@43780
    41
wenzelm@43780
    42
  /* named entries */
wenzelm@43780
    43
wenzelm@43780
    44
  type Entry = (java.lang.String, java.lang.String)
wenzelm@43780
    45
  type T = List[Entry]
wenzelm@43780
    46
wenzelm@43780
    47
  class String(val name: java.lang.String)
wenzelm@43780
    48
  {
wenzelm@43780
    49
    def apply(value: java.lang.String): T = List((name, value))
wenzelm@43780
    50
    def unapply(props: T): Option[java.lang.String] =
wenzelm@43780
    51
      props.find(_._1 == name).map(_._2)
wenzelm@43780
    52
  }
wenzelm@43780
    53
wenzelm@43780
    54
  class Int(name: java.lang.String)
wenzelm@43780
    55
  {
wenzelm@43780
    56
    def apply(value: scala.Int): T = List((name, Value.Int(value)))
wenzelm@43780
    57
    def unapply(props: T): Option[scala.Int] =
wenzelm@43780
    58
      props.find(_._1 == name) match {
wenzelm@43780
    59
        case None => None
wenzelm@43780
    60
        case Some((_, value)) => Value.Int.unapply(value)
wenzelm@43780
    61
      }
wenzelm@43780
    62
  }
wenzelm@43780
    63
wenzelm@43780
    64
  class Long(name: java.lang.String)
wenzelm@43780
    65
  {
wenzelm@43780
    66
    def apply(value: scala.Long): T = List((name, Value.Long(value)))
wenzelm@43780
    67
    def unapply(props: T): Option[scala.Long] =
wenzelm@43780
    68
      props.find(_._1 == name) match {
wenzelm@43780
    69
        case None => None
wenzelm@43780
    70
        case Some((_, value)) => Value.Long.unapply(value)
wenzelm@43780
    71
      }
wenzelm@43780
    72
  }
wenzelm@43780
    73
wenzelm@43780
    74
  class Double(name: java.lang.String)
wenzelm@43780
    75
  {
wenzelm@43780
    76
    def apply(value: scala.Double): T = List((name, Value.Double(value)))
wenzelm@43780
    77
    def unapply(props: T): Option[scala.Double] =
wenzelm@43780
    78
      props.find(_._1 == name) match {
wenzelm@43780
    79
        case None => None
wenzelm@43780
    80
        case Some((_, value)) => Value.Double.unapply(value)
wenzelm@43780
    81
      }
wenzelm@43780
    82
  }
wenzelm@43780
    83
}
wenzelm@43780
    84