author | wenzelm |
Mon, 30 May 2022 10:52:00 +0200 | |
changeset 75489 | f08fd5048df3 |
parent 75393 | 87ebf5a50283 |
child 75794 | 1c3c31319974 |
permissions | -rw-r--r-- |
43780 | 1 |
/* Title: Pure/General/properties.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Property lists. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
75393 | 10 |
object Properties { |
65624 | 11 |
/* entries */ |
12 |
||
43780 | 13 |
type Entry = (java.lang.String, java.lang.String) |
14 |
type T = List[Entry] |
|
15 |
||
75393 | 16 |
object Eq { |
73715
bf51c23f3f99
clarified signature -- avoid odd warning about scala/bug#6675;
wenzelm
parents:
73712
diff
changeset
|
17 |
def apply(a: java.lang.String, b: java.lang.String): java.lang.String = a + "=" + b |
bf51c23f3f99
clarified signature -- avoid odd warning about scala/bug#6675;
wenzelm
parents:
73712
diff
changeset
|
18 |
def apply(entry: Entry): java.lang.String = apply(entry._1, entry._2) |
73712 | 19 |
|
75393 | 20 |
def unapply(str: java.lang.String): Option[Entry] = { |
73712 | 21 |
val i = str.indexOf('=') |
22 |
if (i <= 0) None else Some((str.substring(0, i), str.substring(i + 1))) |
|
23 |
} |
|
24 |
} |
|
25 |
||
64358 | 26 |
def defined(props: T, name: java.lang.String): java.lang.Boolean = |
27 |
props.exists({ case (x, _) => x == name }) |
|
28 |
||
29 |
def get(props: T, name: java.lang.String): Option[java.lang.String] = |
|
30 |
props.collectFirst({ case (x, y) if x == name => y }) |
|
31 |
||
75393 | 32 |
def put(props: T, entry: Entry): T = { |
64358 | 33 |
val (x, y) = entry |
34 |
def update(ps: T): T = |
|
35 |
ps match { |
|
36 |
case (p @ (x1, _)) :: rest => |
|
37 |
if (x1 == x) (x1, y) :: rest else p :: update(rest) |
|
38 |
case Nil => Nil |
|
39 |
} |
|
40 |
if (defined(props, x)) update(props) else entry :: props |
|
41 |
} |
|
42 |
||
43 |
||
65857 | 44 |
/* external storage */ |
45 |
||
46 |
def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps))) |
|
47 |
||
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
48 |
def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T = |
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
49 |
cache.props(XML.Decode.properties(YXML.parse_body(bs.text))) |
65857 | 50 |
|
68018 | 51 |
def compress(ps: List[T], |
52 |
options: XZ.Options = XZ.options(), |
|
75393 | 53 |
cache: XZ.Cache = XZ.Cache() |
54 |
): Bytes = { |
|
65857 | 55 |
if (ps.isEmpty) Bytes.empty |
68018 | 56 |
else { |
57 |
Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))). |
|
58 |
compress(options = options, cache = cache) |
|
59 |
} |
|
65857 | 60 |
} |
61 |
||
75393 | 62 |
def uncompress(bs: Bytes, cache: XML.Cache = XML.Cache.none): List[T] = { |
72885 | 63 |
if (bs.is_empty) Nil |
65857 | 64 |
else { |
68018 | 65 |
val ps = |
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
66 |
XML.Decode.list(XML.Decode.properties)( |
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
67 |
YXML.parse_body(bs.uncompress(cache = cache.xz).text)) |
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
68 |
if (cache.no_cache) ps else ps.map(cache.props) |
65857 | 69 |
} |
70 |
} |
|
71 |
||
72 |
||
65624 | 73 |
/* multi-line entries */ |
74 |
||
65932 | 75 |
def encode_lines(props: T): T = props.map({ case (a, b) => (a, Library.encode_lines(b)) }) |
76 |
def decode_lines(props: T): T = props.map({ case (a, b) => (a, Library.decode_lines(b)) }) |
|
65624 | 77 |
|
78 |
def lines_nonempty(x: java.lang.String, ys: List[java.lang.String]): Properties.T = |
|
79 |
if (ys.isEmpty) Nil else List((x, cat_lines(ys))) |
|
80 |
||
81 |
||
82 |
/* entry types */ |
|
64358 | 83 |
|
75393 | 84 |
class String(val name: java.lang.String) { |
43780 | 85 |
def apply(value: java.lang.String): T = List((name, value)) |
86 |
def unapply(props: T): Option[java.lang.String] = |
|
87 |
props.find(_._1 == name).map(_._2) |
|
72137 | 88 |
def get(props: T): java.lang.String = unapply(props).getOrElse("") |
43780 | 89 |
} |
90 |
||
75393 | 91 |
class Boolean(val name: java.lang.String) { |
48344 | 92 |
def apply(value: scala.Boolean): T = List((name, Value.Boolean(value))) |
93 |
def unapply(props: T): Option[scala.Boolean] = |
|
94 |
props.find(_._1 == name) match { |
|
95 |
case None => None |
|
96 |
case Some((_, value)) => Value.Boolean.unapply(value) |
|
97 |
} |
|
72137 | 98 |
def get(props: T): scala.Boolean = unapply(props).getOrElse(false) |
48344 | 99 |
} |
100 |
||
75393 | 101 |
class Int(val name: java.lang.String) { |
43780 | 102 |
def apply(value: scala.Int): T = List((name, Value.Int(value))) |
103 |
def unapply(props: T): Option[scala.Int] = |
|
104 |
props.find(_._1 == name) match { |
|
105 |
case None => None |
|
106 |
case Some((_, value)) => Value.Int.unapply(value) |
|
107 |
} |
|
72137 | 108 |
def get(props: T): scala.Int = unapply(props).getOrElse(0) |
43780 | 109 |
} |
110 |
||
75393 | 111 |
class Long(val name: java.lang.String) { |
43780 | 112 |
def apply(value: scala.Long): T = List((name, Value.Long(value))) |
113 |
def unapply(props: T): Option[scala.Long] = |
|
114 |
props.find(_._1 == name) match { |
|
115 |
case None => None |
|
116 |
case Some((_, value)) => Value.Long.unapply(value) |
|
117 |
} |
|
72137 | 118 |
def get(props: T): scala.Long = unapply(props).getOrElse(0) |
43780 | 119 |
} |
120 |
||
75393 | 121 |
class Double(val name: java.lang.String) { |
43780 | 122 |
def apply(value: scala.Double): T = List((name, Value.Double(value))) |
123 |
def unapply(props: T): Option[scala.Double] = |
|
124 |
props.find(_._1 == name) match { |
|
125 |
case None => None |
|
126 |
case Some((_, value)) => Value.Double.unapply(value) |
|
127 |
} |
|
72137 | 128 |
def get(props: T): scala.Double = unapply(props).getOrElse(0.0) |
43780 | 129 |
} |
130 |
} |