-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - fix(widget): workaround for webview rendering bug #3997
Conversation
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 ```
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Feel free to merge when you're done with testing.
bors d+
("white-space", "pre-wrap"), | ||
("vertical-align", "top") | ||
], | ||
(a,rest) ← get_block_attrs a, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A related question: does
[style [("x", "y")], className "a", style [("z", "w")], className "b"]
do the right thing?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yes it does
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
it does a merge of the styles
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
and classNames
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So it's equal to [style [("x","y"), ("z","w")], className "a b"]
when it gets emitted.
✌️ EdAyers can now approve this pull request. To approve and merge a pull request, simply reply with |
Sorry for requesting a review I didn't refresh |
Ok I can't find any awful new bugs. |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
bors r+ |
Not sure if it's a github issue or if maybe the draft status confused bors. Let's try again: |
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>
Pull request successfully merged into master. Build succeeded: |
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>
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>
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: