# HG changeset patch
# User wenzelm
# Date 1607170776 -3600
# Node ID af1bd8f2760fc41ef80c47b2efc49afa971cd3f3
# Parent  0f01783400b20ee9d7c18a8b63a292acb0b3513a
clarified signature;

diff -r 0f01783400b2 -r af1bd8f2760f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 05 13:12:18 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 05 13:19:36 2020 +0100
@@ -538,17 +538,27 @@
     val init: Snapshot = State.init.snapshot()
   }
 
-  abstract class Snapshot(
+  abstract class Snapshot private[Document](
     val state: State,
     val version: Version,
-    val is_outdated: Boolean,
     val node_name: Node.Name,
-    val snippet_command: Option[Command])
+    edits: List[Text.Edit],
+    snippet_command: Option[Command])
   {
-    def convert(i: Text.Offset): Text.Offset
-    def revert(i: Text.Offset): Text.Offset
-    def convert(range: Text.Range): Text.Range
-    def revert(range: Text.Range): Text.Range
+    /* edits */
+
+    def is_outdated: Boolean = edits.nonEmpty
+
+    private lazy val reverse_edits = edits.reverse
+
+    def convert(offset: Text.Offset): Text.Offset =
+      (offset /: edits)((i, edit) => edit.convert(i))
+    def revert(offset: Text.Offset): Text.Offset =
+      (offset /: reverse_edits)((i, edit) => edit.revert(i))
+
+    def convert(range: Text.Range): Text.Range = range.map(convert)
+    def revert(range: Text.Range): Text.Range = range.map(revert)
+
 
     def node: Node
     def nodes: List[(Node.Name, Node)]
@@ -1103,6 +1113,7 @@
       /* pending edits and unstable changes */
 
       val stable = recent_stable
+      val version = stable.version.get_finished
 
       val rev_pending_changes =
         for {
@@ -1116,23 +1127,11 @@
           case (edits, Node.Edits(es)) => es ::: edits
           case (edits, _) => edits
         })
-      lazy val reverse_edits = edits.reverse
 
-      new Snapshot(
-        state = this,
-        version = stable.version.get_finished,
-        is_outdated = edits.nonEmpty,
-        node_name = node_name,
-        snippet_command = snippet_command)
+      new Snapshot(this, version, node_name, edits, snippet_command)
       {
         /* local node content */
 
-        def convert(offset: Text.Offset): Text.Offset = (offset /: edits)((i, edit) => edit.convert(i))
-        def revert(offset: Text.Offset): Text.Offset = (offset /: reverse_edits)((i, edit) => edit.revert(i))
-
-        def convert(range: Text.Range): Text.Range = range.map(convert)
-        def revert(range: Text.Range): Text.Range = range.map(revert)
-
         val node: Node = version.nodes(node_name)
 
         def nodes: List[(Node.Name, Node)] =