# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1714759901 -7200
# Node ID de94fcfbc3cef45a72d441764d778a4162479224
# Parent  c9e8461dd5f246d36ebc74ae726cb3f90cd1a60d
lsp: tuned;

diff -r c9e8461dd5f2 -r de94fcfbc3ce src/Pure/General/json.scala
--- 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 {
diff -r c9e8461dd5f2 -r de94fcfbc3ce src/Tools/VSCode/src/lsp.scala
--- 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
       }
   }