This PR adds a new modal for finding elements in the currently opened project. This makes it much easier to find excactly the location/edge/component/update/sync etc that you need. Searches accepts regular expressions (java's regex, so users will have to manually escape special characters). If a search is not a valid regex, it will simply default to string-include.
The modal can be summoned either by selecting view > search... or by pressing ctrl + f.
Additionally, I have included some changes that makes it much easier to navigate the model when using a trackpad.
Right now, to keep the modal performant, it will only show a maximum of 100 (hardcoded) search results, with a priority of components, then locations, then edges. This might not be very accurate, but it's a quick and easy solution that seems to be good enough. In any case, it can be extended and/or refactored fairly easily.
Feature - search project modal
This PR adds a new modal for finding elements in the currently opened project. This makes it much easier to find excactly the location/edge/component/update/sync etc that you need. Searches accepts regular expressions (java's regex, so users will have to manually escape special characters). If a search is not a valid regex, it will simply default to string-include.
The modal can be summoned either by selecting
view
>search...
or by pressingctrl + f
.Additionally, I have included some changes that makes it much easier to navigate the model when using a trackpad.
Dependencies
This PR is based on the changes from https://github.com/DEIS-Tools/H-Uppaal/pull/52, so that should be merged first
Demo
https://user-images.githubusercontent.com/4085393/204058194-fbb49e3b-8e96-43ec-b2f2-a7431d6aac61.mov
Limitations
Right now, to keep the modal performant, it will only show a maximum of 100 (hardcoded) search results, with a priority of components, then locations, then edges. This might not be very accurate, but it's a quick and easy solution that seems to be good enough. In any case, it can be extended and/or refactored fairly easily.