--- 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
--- 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)
--- 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)