author | wenzelm |
Sat, 05 Dec 2020 20:40:24 +0100 | |
changeset 72829 | a28a4105883f |
parent 72828 | 18bc50e58e38 |
child 72830 | ec0d3a62bb3b |
--- 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 */