Playground awkwardly highlights text when focus() is called
See this gif: When I click the "focus" rectangles on the far left side, then the entire section gets highlighted, even if this means moving the editor, which is confusing. When I do this on the right side, the left side's part gets highlighted, which also creates strange focus areas.
My quick guess is that this was introduced here: https://github.com/quantified-uncertainty/squiggle/pull/3262
When I do this on the right side, the left side's part gets highlighted, which also creates strange focus areas.
This part was intentional, and I mentioned the possible risk in this comment. But I understand it can be controversial.
I don't care too much about selecting the text or not (I think selecting can be preferred in some cases, e.g. if you want to cur or delete, but it's hard to guess the user's intention), but I do like the highlighting.
Maybe the right thing to do is 0.5-second yellow color flash of the entire area in the edtior when the variable is selected on the right side, without scrolling.
Something like "on the first click in the viewer, flash; on the second click, select the text" also would be useful.
The 0.5-s flash seems good.
Also, there's the issue that it seems like we don't scroll to the top of the code.
When pressing the button on the sidebar on the left, that also ideally wouldn't reposition the left side. Only right side actions should auto-move the left side like that.