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 */