# 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
       }