mathlib
d4484a4e - fix(widget): workaround for webview rendering bug (#3997)

Commit
5 years ago
fix(widget): workaround for webview rendering bug (#3997) See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/extension.20performance The bug seems to go away if we collapse the extra nested spans made by `block` in to one span. Still should do some tests to make sure this doesn't break anything else. Minimal breaking example is: ``` import tactic.interactive_expr example : 0+1+2+3+4+5+6+7+8+9 + 0+1+2+3+4+5+6+7+8+9 = 0+1+2+3+4+5+6+7+8+9 := by skip ``` Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
Author
Parents
Loading