equal
deleted
inserted
replaced
266 } |
266 } |
267 |
267 |
268 |
268 |
269 /* proper values */ |
269 /* proper values */ |
270 |
270 |
271 def proper[A](x: A): Option[A] = |
|
272 if (x == null) None else Some(x) |
|
273 |
|
274 def proper_string(s: String): Option[String] = |
271 def proper_string(s: String): Option[String] = |
275 if (s == null || s == "") None else Some(s) |
272 if (s == null || s == "") None else Some(s) |
276 |
273 |
277 def proper_list[A](list: List[A]): Option[List[A]] = |
274 def proper_list[A](list: List[A]): Option[List[A]] = |
278 if (list == null || list.isEmpty) None else Some(list) |
275 if (list == null || list.isEmpty) None else Some(list) |