# HG changeset patch
# User wenzelm
# Date 1607169706 -3600
# Node ID 55792cb3892f56a88e8255286dfb43d0a4d56af6
# Parent  1c378ab75d4846b84ede80a368ba31e083e92080
clarified signature;

diff -r 1c378ab75d48 -r 55792cb3892f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 05 12:43:21 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 05 13:01:46 2020 +0100
@@ -531,25 +531,25 @@
   }
 
 
-  /* snapshot */
+  /* snapshot: persistent user-view of document state */
 
   object Snapshot
   {
     val init: Snapshot = State.init.snapshot()
   }
 
-  abstract class Snapshot
+  abstract class Snapshot(
+    val state: State,
+    val version: Version,
+    val is_outdated: Boolean,
+    val node_name: Node.Name,
+    val snippet_command: Option[Command])
   {
-    def state: State
-    def version: Version
-    def 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
 
-    def node_name: Node.Name
     def node: Node
     def nodes: List[(Node.Name, Node)]
 
@@ -557,10 +557,8 @@
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
 
-    def get_snippet_command: Option[Command]
-
     def node_files: List[Node.Name] =
-      get_snippet_command match {
+      snippet_command match {
         case None => List(node_name)
         case Some(command) => node_name :: command.blobs_names
       }
@@ -582,7 +580,7 @@
           .define_version(version1, state0.the_assignment(version))
           .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
 
-      state1.snapshot(name = node_name, snippet_command = Some(command))
+      state1.snapshot(node_name = node_name, snippet_command = Some(command))
     }
 
     def xml_markup(
@@ -591,7 +589,7 @@
 
     def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full): List[XML.Body] =
     {
-      get_snippet_command match {
+      snippet_command match {
         case None => Nil
         case Some(command) =>
           for (Exn.Res(blob) <- command.blobs)
@@ -867,7 +865,7 @@
             Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name,
               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - command1.id)
-          val snapshot = state1.snapshot(name = node_name).command_snippet(command1)
+          val snapshot = state1.snapshot(node_name = node_name).command_snippet(command1)
           (snapshot, state1)
       }
 
@@ -1097,9 +1095,8 @@
         it.hasNext && command_states(version, it.next).exists(_.consolidated)
       }
 
-    // persistent user-view
     def snapshot(
-      name: Node.Name = Node.Name.empty,
+      node_name: Node.Name = Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil,
       snippet_command: Option[Command] = None): Snapshot =
     {
@@ -1112,8 +1109,8 @@
       val rev_pending_changes =
         for {
           change <- history.undo_list.takeWhile(_ != stable)
-          (a, edits) <- change.rev_edits
-          if a == name
+          (name, edits) <- change.rev_edits
+          if name == node_name
         } yield edits
 
       val edits =
@@ -1123,15 +1120,13 @@
         })
       lazy val reverse_edits = edits.reverse
 
-      new Snapshot
+      new Snapshot(
+        state = this,
+        version = stable.version.get_finished,
+        is_outdated = pending_edits.nonEmpty || latest != stable,
+        node_name = node_name,
+        snippet_command = snippet_command)
       {
-        /* global information */
-
-        val state: State = State.this
-        val version: Version = stable.version.get_finished
-        val is_outdated: Boolean = pending_edits.nonEmpty || latest != stable
-
-
         /* local node content */
 
         def convert(offset: Text.Offset): Text.Offset = (offset /: edits)((i, edit) => edit.convert(i))
@@ -1140,8 +1135,7 @@
         def convert(range: Text.Range): Text.Range = range.map(convert)
         def revert(range: Text.Range): Text.Range = range.map(revert)
 
-        val node_name: Node.Name = name
-        val node: Node = version.nodes(name)
+        val node: Node = version.nodes(node_name)
 
         def nodes: List[(Node.Name, Node)] =
           (node_name :: node.load_commands.flatMap(_.blobs_names)).
@@ -1171,8 +1165,6 @@
           }
           else version.nodes.commands_loading(other_node_name).headOption
 
-        def get_snippet_command: Option[Command] = snippet_command
-
         def xml_markup(
             range: Text.Range = Text.Range.full,
             elements: Markup.Elements = Markup.Elements.full): XML.Body =