author | wenzelm |
Sat, 27 Feb 2016 16:37:47 +0100 | |
changeset 62433 | 2436a02f28c4 |
parent 57909 | 0fb331032f02 |
child 63805 | c272680df665 |
permissions | -rw-r--r-- |
43780 | 1 |
/* Title: Pure/General/properties.scala |
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset
|
2 |
Module: PIDE |
43780 | 3 |
Author: Makarius |
4 |
||
5 |
Property lists. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
11 |
object Properties |
|
12 |
{ |
|
13 |
/* plain values */ |
|
14 |
||
15 |
object Value |
|
16 |
{ |
|
48344 | 17 |
object Boolean |
18 |
{ |
|
19 |
def apply(x: scala.Boolean): java.lang.String = x.toString |
|
20 |
def unapply(s: java.lang.String): Option[scala.Boolean] = |
|
21 |
s match { |
|
22 |
case "true" => Some(true) |
|
23 |
case "false" => Some(false) |
|
24 |
case _ => None |
|
25 |
} |
|
62433 | 26 |
def parse(s: java.lang.String): scala.Boolean = |
27 |
unapply(s) getOrElse error("Bad boolean: " + quote(s)) |
|
48344 | 28 |
} |
29 |
||
43780 | 30 |
object Int |
31 |
{ |
|
57909
0fb331032f02
more compact representation of special string values;
wenzelm
parents:
50946
diff
changeset
|
32 |
def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x) |
43780 | 33 |
def unapply(s: java.lang.String): Option[scala.Int] = |
34 |
try { Some(Integer.parseInt(s)) } |
|
35 |
catch { case _: NumberFormatException => None } |
|
62433 | 36 |
def parse(s: java.lang.String): scala.Int = |
37 |
unapply(s) getOrElse error("Bad integer: " + quote(s)) |
|
43780 | 38 |
} |
39 |
||
40 |
object Long |
|
41 |
{ |
|
57909
0fb331032f02
more compact representation of special string values;
wenzelm
parents:
50946
diff
changeset
|
42 |
def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x) |
43780 | 43 |
def unapply(s: java.lang.String): Option[scala.Long] = |
44 |
try { Some(java.lang.Long.parseLong(s)) } |
|
45 |
catch { case _: NumberFormatException => None } |
|
62433 | 46 |
def parse(s: java.lang.String): scala.Long = |
47 |
unapply(s) getOrElse error("Bad integer: " + quote(s)) |
|
43780 | 48 |
} |
49 |
||
50 |
object Double |
|
51 |
{ |
|
52 |
def apply(x: scala.Double): java.lang.String = x.toString |
|
53 |
def unapply(s: java.lang.String): Option[scala.Double] = |
|
54 |
try { Some(java.lang.Double.parseDouble(s)) } |
|
55 |
catch { case _: NumberFormatException => None } |
|
62433 | 56 |
def parse(s: java.lang.String): scala.Double = |
57 |
unapply(s) getOrElse error("Bad real: " + quote(s)) |
|
43780 | 58 |
} |
59 |
} |
|
60 |
||
61 |
||
62 |
/* named entries */ |
|
63 |
||
64 |
type Entry = (java.lang.String, java.lang.String) |
|
65 |
type T = List[Entry] |
|
66 |
||
67 |
class String(val name: java.lang.String) |
|
68 |
{ |
|
69 |
def apply(value: java.lang.String): T = List((name, value)) |
|
70 |
def unapply(props: T): Option[java.lang.String] = |
|
71 |
props.find(_._1 == name).map(_._2) |
|
72 |
} |
|
73 |
||
48344 | 74 |
class Boolean(val name: java.lang.String) |
75 |
{ |
|
76 |
def apply(value: scala.Boolean): T = List((name, Value.Boolean(value))) |
|
77 |
def unapply(props: T): Option[scala.Boolean] = |
|
78 |
props.find(_._1 == name) match { |
|
79 |
case None => None |
|
80 |
case Some((_, value)) => Value.Boolean.unapply(value) |
|
81 |
} |
|
82 |
} |
|
83 |
||
48015 | 84 |
class Int(val name: java.lang.String) |
43780 | 85 |
{ |
86 |
def apply(value: scala.Int): T = List((name, Value.Int(value))) |
|
87 |
def unapply(props: T): Option[scala.Int] = |
|
88 |
props.find(_._1 == name) match { |
|
89 |
case None => None |
|
90 |
case Some((_, value)) => Value.Int.unapply(value) |
|
91 |
} |
|
92 |
} |
|
93 |
||
48015 | 94 |
class Long(val name: java.lang.String) |
43780 | 95 |
{ |
96 |
def apply(value: scala.Long): T = List((name, Value.Long(value))) |
|
97 |
def unapply(props: T): Option[scala.Long] = |
|
98 |
props.find(_._1 == name) match { |
|
99 |
case None => None |
|
100 |
case Some((_, value)) => Value.Long.unapply(value) |
|
101 |
} |
|
102 |
} |
|
103 |
||
48015 | 104 |
class Double(val name: java.lang.String) |
43780 | 105 |
{ |
106 |
def apply(value: scala.Double): T = List((name, Value.Double(value))) |
|
107 |
def unapply(props: T): Option[scala.Double] = |
|
108 |
props.find(_._1 == name) match { |
|
109 |
case None => None |
|
110 |
case Some((_, value)) => Value.Double.unapply(value) |
|
111 |
} |
|
112 |
} |
|
113 |
} |
|
114 |