avoid duplicate entries: snippet_command is defined within node;
authorwenzelm
Sat, 05 Dec 2020 20:40:24 +0100
changeset 72829 a28a4105883f
parent 72828 18bc50e58e38
child 72830 ec0d3a62bb3b
avoid duplicate entries: snippet_command is defined within node;
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 */