## Stream: general

### Topic: widget rendering bug

#### Scott Morrison (Sep 24 2020 at 06:36):

Hi @Edward Ayers, just letting you know about a widget rendering bug:
If you look at the (wildly in progress) opens_le_cover branch, on commit 0c329591c6a20ebd252df92966ba94af88a1129b, line 135 of category_theory.limits.cofinal, the goal displays as

⊢ 𝟭 (cocone (F ⋙ G)  ≅ extend_cocone ⋙ cocones.whiskering F
)


(the close parenthesis has gone stray).

#### Edward Ayers (Sep 24 2020 at 07:16):

Oof. I'll have a look

#### Edward Ayers (Sep 24 2020 at 07:19):

Does it change if you make the window bigger and smaller?

#### Edward Ayers (Sep 24 2020 at 07:22):

It's rendering ok for me :/ maybe I'm missing something?
image.png
image.png

#### Edward Ayers (Sep 24 2020 at 07:23):

I've seen this failure mode before though

#### Kenny Lau (Sep 24 2020 at 07:23):

I've seen this bug too

#### Edward Ayers (Sep 24 2020 at 07:25):

Whats happening is the (cocone (F ⋙ G)) element is wrapped in an inline-block to get the pretty linebreaking to work, but sometimes the layout maths is off and it linebreaks in this block before the outer one linebreaks

#### Edward Ayers (Sep 24 2020 at 07:25):

Maybe it only happens for certain fonts

#### Edward Ayers (Sep 24 2020 at 07:25):

What fonts are you guys using?

#### Edward Ayers (Sep 24 2020 at 07:43):

Ok I've tried changing the fonts etc and I can't get this theorem to exhibit this bug, so I'll keep programming until I find an example of the bug and then try to diagnose it. Hopefully the bug doesn't arise too frequently to be a massive issue in the mean time.

#### Gabriel Ebner (Sep 24 2020 at 08:03):

Another funny rendering bug is that λ (n : ℕ), n > n breaks like this:

λ (n : ℕ)
, n > n


In the API documentation we solve these issues by post-processing the formatted expression a little bit, i.e. move parenthesis inside: https://github.com/leanprover-community/doc-gen/blob/fe4f42fdda23b690695b40d353e5da6d49cf9d65/src/export_json.lean#L70-L126

Last updated: May 09 2021 at 18:17 UTC