Except two minor remarks, this is great!

Where are those? Since I can't find them, maybe a minor remark of my own :-).

Maybe we should consider what widget in the sidebar gets the focus by default - right now it's the entry (and the tree focus is just one tab or enter press away) but maybe users who use primarily keyboard are more used to having the tree focused. I don't mind much myself as I just use mouse for the tree.

I'd expected that it required more code to make the filter per document but happy to be proven wrong :D.

Same here and it actually applies to the whole patch. I was thinking about this feature for a long time but thinking it would be annoying to do and then saw the pull request which was pretty trivial and mostly working so I got attracted :-).

Gentle prompt, its a UI change and new functionality so manual change also needed.

Sure, if it's something that's going to be merged, I'll definitely update it.

—
Reply to this email directly, view it on GitHub, or unsubscribe.
Triage notifications on the go with GitHub Mobile for iOS or Android.
You are receiving this because you are subscribed to this thread.