filetree plugin: make it possible to filter items in the tree view
Like the one in the Project plugin, it's useful when you have many documents open at the same time.
Like the one in the Project plugin, it's useful when you have many documents open at the same time.