# HG changeset patch
# User wenzelm
# Date 1607171857 -3600
# Node ID 8d166825265e6d09e0068a6d86187d4359cc603e
# Parent  13275ae9e209a2c4980ff19db672773e17477d50
clarified signature;

diff -r 13275ae9e209 -r 8d166825265e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 05 13:29:19 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 05 13:37:37 2020 +0100
@@ -550,6 +550,14 @@
         (if (is_outdated) ", outdated" else "") + ")"
 
 
+    /* nodes */
+
+    val node: Node = version.nodes(node_name)
+
+    def node_files: List[Node.Name] =
+      node_name :: (node.load_commands ::: snippet_command.toList).flatMap(_.blobs_names)
+
+
     /* edits */
 
     def is_outdated: Boolean = edits.nonEmpty
@@ -565,21 +573,6 @@
     def revert(range: Text.Range): Text.Range = range.map(revert)
 
 
-    /* local node content */
-
-    val node: Node = version.nodes(node_name)
-
-    def nodes: List[(Node.Name, Node)] =
-      (node_name :: node.load_commands.flatMap(_.blobs_names)).
-        map(name => (name, version.nodes(name)))
-
-    def node_files: List[Node.Name] =
-      snippet_command match {
-        case None => List(node_name)
-        case Some(command) => node_name :: command.blobs_names
-      }
-
-
     /* theory load commands */
 
     val commands_loading: List[Command] =
diff -r 13275ae9e209 -r 8d166825265e src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sat Dec 05 13:29:19 2020 +0100
+++ b/src/Pure/Tools/update.scala	Sat Dec 05 13:37:37 2020 +0100
@@ -43,7 +43,8 @@
         progress.echo("Processing theory " + args.print_node + " ...")
 
         val snapshot = args.snapshot
-        for ((node_name, node) <- snapshot.nodes) {
+        for (node_name <- snapshot.node_files) {
+          val node = snapshot.version.nodes(node_name)
           val xml =
             snapshot.state.xml_markup(snapshot.version, node_name,
               elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))