Sam Tobin-Hochstadt

That code is getting and setting the values in the preferences file. Then other places are using that value. You might want one of these locations: https://github.com/search?q=repo%3Aracket%2Fgui%20smoothing&type=code

I think the current situation is that a small doc change is needed, plus moving the contents of one file into another. @jsmaniac I'm happy to do that if you...

This would be good to add but I think @rmculpepper would need to be the one to fix the merge conflicts.

This would be nice to have, but we would need a solver for such constraints. Right now refinements use a simple Fourier-Motzkin Elimination-based solver. What would you propose for reals?

Those systems do provide some real number handling, but (a) that's a very large dependency to add and (b) the handling of reals is far from complete (for fundamental undecidability...

That would be a nice addition. I'd be happy to review a patch, or provide guidance on what to work on, to add that. At the moment I'm not likely...

It would only overwrite if there was a new selection, right? I just tried this out in Firefox and it does the overwriting if there's a selection, and continues searching...

Here's what I just did, with chrome on this github page (on Linux): 1. Hit ctrl-f. The search text box is empty. 2. Close the search box. 3. Select "The...