Round brush coordinates

[wch]

This fixes #1634.

[wch]

For future reference, here's a comparison of different methods of rounding numbers in Javascript:

// Round to a specified number of digits after the decimal. 0 means round to
// integer value. Negative values mean round to digits before decimal.
function roundDecimal(x, digits = 0) {
  const n = Math.pow(10, digits);
  return Math.round(x * n) / n;
}

// Round to a specified number of significant digits.
function roundSignif(x, digits = 1) {
  if (digits < 1)
    throw "Significant digits must be 1 or greater";

  const scaleFactor = Math.floor(Math.log10(Math.abs(x)));
  return roundDecimal(x, digits - scaleFactor - 1);
}


for (var precision = 1; precision < 15; precision++) {
  for (var i = 0; i < 10000; i++) {
    let val = Math.pow((Math.random() / Math.random()), 10*Math.random());

    let v1 = roundSignif(val, precision);
    let v2 = parseFloat(val.toPrecision(precision));
    if (v1 !== v2) {
      console.error("Inconsistency found after " + i + " iterations at precision " + precision + ":\n" +
        val + "\n" + v1 + "\n" + v2);
      break;
    }
  }
}

(Also at https://gist.github.com/wch/9d27ddcac1d81101b4708403a096cd31)

Using parseFloat(val.toPrecision(precision)) seems to be less prone to rounding error than other methods that use Math.round().