# HG changeset patch
# User wenzelm
# Date 1671805769 -3600
# Node ID d062c7f4f2d1a9076e57bd82724d69e271358bfc
# Parent  9766a2a571827a88bf14f25cac68c808f788fdbf
tuned;

diff -r 9766a2a57182 -r d062c7f4f2d1 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Dec 23 15:20:53 2022 +0100
+++ b/src/Pure/PIDE/session.scala	Fri Dec 23 15:29:29 2022 +0100
@@ -690,7 +690,7 @@
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
-    get_state().snapshot(name, pending_edits)
+    get_state().snapshot(name, pending_edits = pending_edits)
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
diff -r 9766a2a57182 -r d062c7f4f2d1 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Fri Dec 23 15:20:53 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Fri Dec 23 15:29:29 2022 +0100
@@ -231,7 +231,8 @@
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
   def is_stable: Boolean = pending_edits.isEmpty
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
+  def snapshot(): Document.Snapshot =
+    session.snapshot(node_name, pending_edits = pending_edits)
 
   def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
     new VSCode_Rendering(snapshot, model)
diff -r 9766a2a57182 -r d062c7f4f2d1 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Dec 23 15:20:53 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Dec 23 15:29:29 2022 +0100
@@ -469,7 +469,8 @@
   /* snapshot */
 
   def is_stable: Boolean = pending_edits.isEmpty
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
+  def snapshot(): Document.Snapshot =
+    session.snapshot(node_name, pending_edits = pending_edits)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
@@ -609,7 +610,8 @@
   }
 
   def is_stable: Boolean = !pending_edits.nonEmpty
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
+  def snapshot(): Document.Snapshot =
+    session.snapshot(node_name, pending_edits = pending_edits.get_edits)
 
   def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
     pending_edits.flush_edits(doc_blobs, hidden)