Ethan Merritt - 2013-08-07

This is a reasonable idea, but implementing it would be more work than you may think. The oversampling constant is currently hard-wired into the javascript code associated with mousing. If we make it a parameter to "set term", we also have to rewrite the javascript support routines to look for the current value and use it for all mouse operations. Certainly possible, but a bit tedious and it would introduce a version-dependence for the javascript routines.

Maybe for version 5