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