I have yet to see a good web based text editor with syntax highlighting. They all mess with the native search functionality of the browser. Because they can't just use a textarea for the edit area. With this approach, it would be possible.
I wonder how usable a Python version of this would be?
I slightly expect you to pull a "no true Scotsman" here and suggest it's actually no good because it doesn't really support mobile browsers very well, but Microsoft's Monaco editor that's driven from VS Code is quite good. https://microsoft.github.io/monaco-editor/
When I hit ctrl+f on that page and type "export":
First it says "1 of 4 matches" but nothing is highlighted.
When I hit enter, it says "2 of 4 matches" and again, nothing is highlighted.
When I hit enter again, it says "3 of 4 matches" and the first match is highlighted.
When I hit enter again, it says "4 of 4 matches" and the second match is highlighted.