--- 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] =
--- 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))