# HG changeset patch
# User wenzelm
# Date 1607172309 -3600
# Node ID ab1a49ac456b341615fac7421b8ab9a11e265911
# Parent  8d166825265e6d09e0068a6d86187d4359cc603e
tuned signature;

diff -r 8d166825265e -r ab1a49ac456b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 05 13:37:37 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 05 13:45:09 2020 +0100
@@ -552,7 +552,9 @@
 
     /* nodes */
 
-    val node: Node = version.nodes(node_name)
+    def get_node(name: Node.Name): Node = version.nodes(name)
+
+    val node: Node = get_node(node_name)
 
     def node_files: List[Node.Name] =
       node_name :: (node.load_commands ::: snippet_command.toList).flatMap(_.blobs_names)
@@ -661,8 +663,8 @@
         case None => None
         case Some(st) =>
           val command = st.command
-          val node = version.nodes(command.node_name)
-          if (node.commands.contains(command)) Some((node, command)) else None
+          val command_node = get_node(command.node_name)
+          if (command_node.commands.contains(command)) Some((command_node, command)) else None
       }
 
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
@@ -680,7 +682,7 @@
 
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
       if (other_node_name.is_theory) {
-        val other_node = version.nodes(other_node_name)
+        val other_node = get_node(other_node_name)
         val iterator = other_node.command_iterator(revert(offset) max 0)
         if (iterator.hasNext) {
           val (command0, _) = iterator.next
@@ -705,7 +707,7 @@
     /* command ids: static and dynamic */
 
     def command_id_map: Map[Document_ID.Generic, Command] =
-      state.command_id_map(version, version.nodes(node_name).commands)
+      state.command_id_map(version, get_node(node_name).commands)
 
 
     /* cumulate markup */
diff -r 8d166825265e -r ab1a49ac456b src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Sat Dec 05 13:37:37 2020 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Sat Dec 05 13:45:09 2020 +0100
@@ -84,7 +84,7 @@
               (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
               if props.contains((Markup.INSTANCE, state0.instance))
             } yield elem).toList
-          val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
+          val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd)
           (snapshot, command_results, results, removed)
         case None =>
           (Document.Snapshot.init, Command.Results.empty, Nil, true)
diff -r 8d166825265e -r ab1a49ac456b src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sat Dec 05 13:37:37 2020 +0100
+++ b/src/Pure/Tools/update.scala	Sat Dec 05 13:45:09 2020 +0100
@@ -44,7 +44,7 @@
 
         val snapshot = args.snapshot
         for (node_name <- snapshot.node_files) {
-          val node = snapshot.version.nodes(node_name)
+          val node = snapshot.get_node(node_name)
           val xml =
             snapshot.state.xml_markup(snapshot.version, node_name,
               elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
diff -r 8d166825265e -r ab1a49ac456b src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Dec 05 13:37:37 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Dec 05 13:45:09 2020 +0100
@@ -282,7 +282,7 @@
     pos match {
       case Position.Item_Id(id, range) if range.start > 0 =>
         snapshot.find_command(id) match {
-          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
+          case Some((node, command)) if snapshot.get_node(command.node_name) eq node =>
             node.command_start(command) match {
               case Some(start) => text_offset == start + command.chunk.decode(range.start)
               case None => false
diff -r 8d166825265e -r ab1a49ac456b src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Sat Dec 05 13:37:37 2020 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Sat Dec 05 13:45:09 2020 +0100
@@ -183,7 +183,7 @@
 
     val iterator =
       restriction match {
-        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+        case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
         case None => snapshot.version.nodes.iterator
       }
     val nodes_timing1 =