# HG changeset patch # User wenzelm # Date 1520953693 -3600 # Node ID ff561f6e0a8e2b0131b46d830a3c779aba1d83b7 # Parent ff87225e7e8e464865eeb69910df945b254db1c6 more operations for typed JSON values; diff -r ff87225e7e8e -r ff561f6e0a8e src/Pure/General/json.scala --- a/src/Pure/General/json.scala Tue Mar 13 10:54:40 2018 +0100 +++ b/src/Pure/General/json.scala Tue Mar 13 16:08:13 2018 +0100 @@ -232,7 +232,7 @@ } - /* values */ + /* typed values */ object Value { @@ -281,6 +281,17 @@ case _ => None } } + + object List + { + def unapply[A](json: T, unapply: T => Option[A]): Option[List[A]] = + json match { + case xs: List[T] => + val ys = xs.map(unapply) + if (ys.forall(_.isDefined)) Some(ys.map(_.get)) else None + case _ => None + } + } } @@ -310,25 +321,39 @@ case _ => None } - def array[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] = - for { - a0 <- array(obj, name) - a = a0.map(unapply(_)) - if a.forall(_.isDefined) - } yield a.map(_.get) + def value_default[A](obj: T, name: String, unapply: T => Option[A], default: A): Option[A] = + value(obj, name) match { + case None => Some(default) + case Some(json) => unapply(json) + } def string(obj: T, name: String): Option[String] = value(obj, name, Value.String.unapply) + def string_default(obj: T, name: String, default: String = ""): Option[String] = + value_default(obj, name, Value.String.unapply, default) def double(obj: T, name: String): Option[Double] = value(obj, name, Value.Double.unapply) + def double_default(obj: T, name: String, default: Double = 0.0): Option[Double] = + value_default(obj, name, Value.Double.unapply, default) def long(obj: T, name: String): Option[Long] = value(obj, name, Value.Long.unapply) + def long_default(obj: T, name: String, default: Long = 0): Option[Long] = + value_default(obj, name, Value.Long.unapply, default) def int(obj: T, name: String): Option[Int] = value(obj, name, Value.Int.unapply) + def int_default(obj: T, name: String, default: Int = 0): Option[Int] = + value_default(obj, name, Value.Int.unapply, default) def bool(obj: T, name: String): Option[Boolean] = value(obj, name, Value.Boolean.unapply) + def bool_default(obj: T, name: String, default: Boolean = false): Option[Boolean] = + value_default(obj, name, Value.Boolean.unapply, default) + + def list[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] = + value(obj, name, Value.List.unapply(_, unapply)) + def list_default[A](obj: T, name: String, unapply: T => Option[A], default: List[A] = Nil) + : Option[List[A]] = value_default(obj, name, Value.List.unapply(_, unapply), default) } diff -r ff87225e7e8e -r ff561f6e0a8e src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Tue Mar 13 10:54:40 2018 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Tue Mar 13 16:08:13 2018 +0100 @@ -309,7 +309,7 @@ doc <- JSON.value(params, "textDocument") uri <- JSON.string(doc, "uri") version <- JSON.long(doc, "version") - changes <- JSON.array(params, "contentChanges", unapply_change _) + changes <- JSON.list(params, "contentChanges", unapply_change _) } yield (Url.absolute_file(uri), version, changes) case _ => None }