--- 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 */
--- 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)
--- 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))
--- 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
--- 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 =