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.;
     1 /*  Title:      Pure/General/properties.scala
     2     Author:     Makarius
     3 
     4 Property lists.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Properties
    11 {
    12   /* plain values */
    13 
    14   object Value
    15   {
    16     object Int
    17     {
    18       def apply(x: scala.Int): java.lang.String = x.toString
    19       def unapply(s: java.lang.String): Option[scala.Int] =
    20         try { Some(Integer.parseInt(s)) }
    21         catch { case _: NumberFormatException => None }
    22     }
    23 
    24     object Long
    25     {
    26       def apply(x: scala.Long): java.lang.String = x.toString
    27       def unapply(s: java.lang.String): Option[scala.Long] =
    28         try { Some(java.lang.Long.parseLong(s)) }
    29         catch { case _: NumberFormatException => None }
    30     }
    31 
    32     object Double
    33     {
    34       def apply(x: scala.Double): java.lang.String = x.toString
    35       def unapply(s: java.lang.String): Option[scala.Double] =
    36         try { Some(java.lang.Double.parseDouble(s)) }
    37         catch { case _: NumberFormatException => None }
    38     }
    39   }
    40 
    41 
    42   /* named entries */
    43 
    44   type Entry = (java.lang.String, java.lang.String)
    45   type T = List[Entry]
    46 
    47   class String(val name: java.lang.String)
    48   {
    49     def apply(value: java.lang.String): T = List((name, value))
    50     def unapply(props: T): Option[java.lang.String] =
    51       props.find(_._1 == name).map(_._2)
    52   }
    53 
    54   class Int(name: java.lang.String)
    55   {
    56     def apply(value: scala.Int): T = List((name, Value.Int(value)))
    57     def unapply(props: T): Option[scala.Int] =
    58       props.find(_._1 == name) match {
    59         case None => None
    60         case Some((_, value)) => Value.Int.unapply(value)
    61       }
    62   }
    63 
    64   class Long(name: java.lang.String)
    65   {
    66     def apply(value: scala.Long): T = List((name, Value.Long(value)))
    67     def unapply(props: T): Option[scala.Long] =
    68       props.find(_._1 == name) match {
    69         case None => None
    70         case Some((_, value)) => Value.Long.unapply(value)
    71       }
    72   }
    73 
    74   class Double(name: java.lang.String)
    75   {
    76     def apply(value: scala.Double): T = List((name, Value.Double(value)))
    77     def unapply(props: T): Option[scala.Double] =
    78       props.find(_._1 == name) match {
    79         case None => None
    80         case Some((_, value)) => Value.Double.unapply(value)
    81       }
    82   }
    83 }
    84