s/I created #3015 to/I created #3050 to/ :)

To the topic:

• looks quite good!
• I gave it a quick try and works as advertised.
• I agree on better searching case-insensitive.
• maybe the update of the symbol list on each notebook tab change might be a noticeable performance hit on older machines ("unfortunately" I've recently got a new notebook with a bleeding fast CPU so I won't notice :D).

I see why the update on notebook tab change is necessary; the symbol filter text is static and applies to all documents. I think it would be even better to have filters per document, otherwise it could be confusing if I switch to another document and suddenly the symbol list is empty. After wondering about it, the user will probably realize it's because of the still set filter and then will clear the filter.
Though having per document filters obviously requires much more efforts :(.

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