JFTR, I didn't mean to suggest it should be a per-document filter. Only that it would maybe create the most comfortable solution but also with the most effort needed.

Getting back to @techee's first idea of this feature: when we want tojust jump to the first match of a symbol, it might be enough to enable GTK's treeview search feature (where a little text input field pos up automagically and filters the tree, https://docs.gtk.org/gtk3/method.TreeView.set_enable_search.html).
Then we don't need a permanent visible search field and probably even less code. At the price thata search feature enabled by just typing in a list is less intuitive and might not be recognised by all users.
I didn't try it yet, it's just a thought.

In case someone wants to try, there might be signal handlers on the symbol list to switch focus to the editing widget on any keypress, at least it feels like this.

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