Robby Findler 28ca7c6d14 improve the situation for search results in nested editors ... This doesn't quite fix all the problems, as the outer editor doesn't get callbacks when the position changes in the inner editors (and the inner ones aren't propogating the callbacks currently) so the "n/m matches" display doesn't update properly in that case. Also, it doesn't (yet) try to draw the search bubbles for embedded editors Still, progress has been made; at least the bar is not red anymore when there are hits only in embedded editors closes PR 12786		2016-07-23 03:00:00 -05:00
..
tests	improve the situation for search results in nested editors	2016-07-23 03:00:00 -05:00
info.rkt	Remove extra directories.	2014-12-02 02:33:07 -05:00