src/Pure/PIDE/editor.scala

--- a/src/Pure/PIDE/editor.scala	Tue Jan 31 20:09:03 2023 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Jan 31 20:37:46 2023 +0100
@@ -38,7 +38,7 @@
   }
 
   def document_session(): Document_Editor.Session =
-    document_state().session(() => session.snapshot())
+    document_state().session(session)
 
   def document_required(): List[Document.Node.Name] = {
     val st = document_state()