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