src/Pure/PIDE/document.scala
changeset 72829 a28a4105883f
parent 72823 ab1a49ac456b
child 72844 240c8a0f6337
--- a/src/Pure/PIDE/document.scala	Sat Dec 05 19:30:37 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 05 20:40:24 2020 +0100
@@ -557,7 +557,7 @@
     val node: Node = get_node(node_name)
 
     def node_files: List[Node.Name] =
-      node_name :: (node.load_commands ::: snippet_command.toList).flatMap(_.blobs_names)
+      node_name :: node.load_commands.flatMap(_.blobs_names)
 
 
     /* edits */