--- a/src/Pure/PIDE/document.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 12 11:49:58 2013 +0200
@@ -324,17 +324,23 @@
/** global state -- document structure, execution process, editing history **/
+ object Snapshot
+ {
+ val init = State.init.snapshot()
+ }
+
abstract class Snapshot
{
val state: State
val version: Version
- val node_name: Node.Name
- val node: Node
val is_outdated: Boolean
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
+
+ val node_name: Node.Name
+ val node: Node
def eq_content(other: Snapshot): Boolean
def cumulate_markup[A](
range: Text.Range,
@@ -555,10 +561,10 @@
new Snapshot
{
+ /* global information */
+
val state = State.this
val version = stable.version.get_finished
- val node_name = name
- val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
@@ -566,6 +572,12 @@
def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
+
+ /* local node content */
+
+ val node_name = name
+ val node = version.nodes(name)
+
def eq_content(other: Snapshot): Boolean =
!is_outdated && !other.is_outdated &&
node.commands.size == other.node.commands.size &&