249 case x: java.lang.String => isabelle.UUID.unapply(x) |
249 case x: java.lang.String => isabelle.UUID.unapply(x) |
250 case _ => None |
250 case _ => None |
251 } |
251 } |
252 } |
252 } |
253 |
253 |
254 object String { |
254 object String |
|
255 { |
255 def unapply(json: T): Option[java.lang.String] = |
256 def unapply(json: T): Option[java.lang.String] = |
256 json match { |
257 json match { |
257 case x: java.lang.String => Some(x) |
258 case x: java.lang.String => Some(x) |
258 case _ => None |
259 case _ => None |
259 } |
260 } |
260 } |
261 } |
261 |
262 |
262 object Double { |
263 object Double |
|
264 { |
263 def unapply(json: T): Option[scala.Double] = |
265 def unapply(json: T): Option[scala.Double] = |
264 json match { |
266 json match { |
265 case x: scala.Double => Some(x) |
267 case x: scala.Double => Some(x) |
266 case x: scala.Long => Some(x.toDouble) |
268 case x: scala.Long => Some(x.toDouble) |
267 case x: scala.Int => Some(x.toDouble) |
269 case x: scala.Int => Some(x.toDouble) |
268 case _ => None |
270 case _ => None |
269 } |
271 } |
270 } |
272 } |
271 |
273 |
272 object Long { |
274 object Long |
|
275 { |
273 def unapply(json: T): Option[scala.Long] = |
276 def unapply(json: T): Option[scala.Long] = |
274 json match { |
277 json match { |
275 case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong) |
278 case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong) |
276 case x: scala.Long => Some(x) |
279 case x: scala.Long => Some(x) |
277 case x: scala.Int => Some(x.toLong) |
280 case x: scala.Int => Some(x.toLong) |
278 case _ => None |
281 case _ => None |
279 } |
282 } |
280 } |
283 } |
281 |
284 |
282 object Int { |
285 object Int |
|
286 { |
283 def unapply(json: T): Option[scala.Int] = |
287 def unapply(json: T): Option[scala.Int] = |
284 json match { |
288 json match { |
285 case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt) |
289 case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt) |
286 case x: scala.Long if x.toInt.toLong == x => Some(x.toInt) |
290 case x: scala.Long if x.toInt.toLong == x => Some(x.toInt) |
287 case x: scala.Int => Some(x) |
291 case x: scala.Int => Some(x) |
288 case _ => None |
292 case _ => None |
289 } |
293 } |
290 } |
294 } |
291 |
295 |
292 object Boolean { |
296 object Boolean |
|
297 { |
293 def unapply(json: T): Option[scala.Boolean] = |
298 def unapply(json: T): Option[scala.Boolean] = |
294 json match { |
299 json match { |
295 case x: scala.Boolean => Some(x) |
300 case x: scala.Boolean => Some(x) |
296 case _ => None |
301 case _ => None |
297 } |
302 } |