# HG changeset patch
# User wenzelm
# Date 1607197224 -3600
# Node ID a28a4105883f438449b8541a79b41f2f7ebeb29a
# Parent  18bc50e58e38c4dac45c83de6dc89acf2ebac424
avoid duplicate entries: snippet_command is defined within node;

diff -r 18bc50e58e38 -r a28a4105883f src/Pure/PIDE/document.scala
--- 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 */