--- a/src/Pure/General/json.scala Fri May 03 11:10:58 2024 +0200
+++ b/src/Pure/General/json.scala Fri May 03 20:11:41 2024 +0200
@@ -25,7 +25,7 @@
type T = Map[String, JSON.T]
val empty: Object.T = Map.empty
- def apply(entries: Entry*): Object.T = Map(entries:_*)
+ def apply(entries: Entry*): Object.T = entries.toMap
def unapply(obj: Any): Option[Object.T] =
obj match {
--- a/src/Tools/VSCode/src/lsp.scala Fri May 03 11:10:58 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala Fri May 03 20:11:41 2024 +0200
@@ -528,9 +528,7 @@
def unapply(json: JSON.T): Option[Double] =
json match {
case Notification("PIDE/output_set_margin", Some(params)) =>
- for {
- margin <- JSON.double(params, "margin")
- } yield (margin)
+ JSON.double(params, "margin")
case _ => None
}
}