1/* Title: Pure/General/properties.scala 2 Author: Makarius 3 4Property lists. 5*/ 6 7package isabelle 8 9 10object Properties 11{ 12 /* entries */ 13 14 type Entry = (java.lang.String, java.lang.String) 15 type T = List[Entry] 16 17 def defined(props: T, name: java.lang.String): java.lang.Boolean = 18 props.exists({ case (x, _) => x == name }) 19 20 def get(props: T, name: java.lang.String): Option[java.lang.String] = 21 props.collectFirst({ case (x, y) if x == name => y }) 22 23 def put(props: T, entry: Entry): T = 24 { 25 val (x, y) = entry 26 def update(ps: T): T = 27 ps match { 28 case (p @ (x1, _)) :: rest => 29 if (x1 == x) (x1, y) :: rest else p :: update(rest) 30 case Nil => Nil 31 } 32 if (defined(props, x)) update(props) else entry :: props 33 } 34 35 36 /* external storage */ 37 38 def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps))) 39 40 def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T = 41 { 42 val ps = XML.Decode.properties(YXML.parse_body(bs.text)) 43 xml_cache match { 44 case None => ps 45 case Some(cache) => cache.props(ps) 46 } 47 } 48 49 def compress(ps: List[T], 50 options: XZ.Options = XZ.options(), 51 cache: XZ.Cache = XZ.cache()): Bytes = 52 { 53 if (ps.isEmpty) Bytes.empty 54 else { 55 Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))). 56 compress(options = options, cache = cache) 57 } 58 } 59 60 def uncompress(bs: Bytes, 61 cache: XZ.Cache = XZ.cache(), 62 xml_cache: Option[XML.Cache] = None): List[T] = 63 { 64 if (bs.isEmpty) Nil 65 else { 66 val ps = 67 XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text)) 68 xml_cache match { 69 case None => ps 70 case Some(cache) => ps.map(cache.props(_)) 71 } 72 } 73 } 74 75 76 /* multi-line entries */ 77 78 def encode_lines(props: T): T = props.map({ case (a, b) => (a, Library.encode_lines(b)) }) 79 def decode_lines(props: T): T = props.map({ case (a, b) => (a, Library.decode_lines(b)) }) 80 81 def lines_nonempty(x: java.lang.String, ys: List[java.lang.String]): Properties.T = 82 if (ys.isEmpty) Nil else List((x, cat_lines(ys))) 83 84 85 /* entry types */ 86 87 class String(val name: java.lang.String) 88 { 89 def apply(value: java.lang.String): T = List((name, value)) 90 def unapply(props: T): Option[java.lang.String] = 91 props.find(_._1 == name).map(_._2) 92 } 93 94 class Boolean(val name: java.lang.String) 95 { 96 def apply(value: scala.Boolean): T = List((name, Value.Boolean(value))) 97 def unapply(props: T): Option[scala.Boolean] = 98 props.find(_._1 == name) match { 99 case None => None 100 case Some((_, value)) => Value.Boolean.unapply(value) 101 } 102 } 103 104 class Int(val name: java.lang.String) 105 { 106 def apply(value: scala.Int): T = List((name, Value.Int(value))) 107 def unapply(props: T): Option[scala.Int] = 108 props.find(_._1 == name) match { 109 case None => None 110 case Some((_, value)) => Value.Int.unapply(value) 111 } 112 } 113 114 class Long(val name: java.lang.String) 115 { 116 def apply(value: scala.Long): T = List((name, Value.Long(value))) 117 def unapply(props: T): Option[scala.Long] = 118 props.find(_._1 == name) match { 119 case None => None 120 case Some((_, value)) => Value.Long.unapply(value) 121 } 122 } 123 124 class Double(val name: java.lang.String) 125 { 126 def apply(value: scala.Double): T = List((name, Value.Double(value))) 127 def unapply(props: T): Option[scala.Double] = 128 props.find(_._1 == name) match { 129 case None => None 130 case Some((_, value)) => Value.Double.unapply(value) 131 } 132 } 133} 134