The question is whether not to even clear it after selecting an item in the symbol tree. The use case for this feature I had in mind was to just get quickly to the right symbol in the tree and navigate to it and not really having the tree filtered permanently (and having to manually clear it later).

Hmm, I tried it but it's strange. So if it's on a per-document basis, the filter string should probably go to GeanyDocumentPrivate.

—
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.