Make line height calculations more tolerant of browser rounding errors

sedwards2009 · marijnh · commit 449eab87b375 · 2017-06-28T10:19:12.000+02:00
diff --git a/src/display/update_lines.js b/src/display/update_lines.js
@@ -21,7 +21,7 @@ export function updateHeightsInViewport(cm) {
     }
     let diff = cur.line.height - height
     if (height < 2) height = textHeight(display)
-    if (diff > .001 || diff < -.001) {
+    if (diff > .005 || diff < -.005) {
       updateLineHeight(cur.line, height)
       updateWidgetHeight(cur.line)
       if (cur.rest) for (let j = 0; j < cur.rest.length; j++)

Original file line number	Diff line number	Diff line change
`@@ -21,7 +21,7 @@ export function updateHeightsInViewport(cm) {`
`21`	`21`	`}`
`22`	`22`	`let diff = cur.line.height - height`
`23`	`23`	`if (height < 2) height = textHeight(display)`
`24`		`- if (diff > .001 \|\| diff < -.001) {`
	`24`	`+ if (diff > .005 \|\| diff < -.005) {`
`25`	`25`	`updateLineHeight(cur.line, height)`
`26`	`26`	`updateWidgetHeight(cur.line)`
`27`	`27`	`if (cur.rest) for (let j = 0; j < cur.rest.length; j++)`