copy code from alectryon

Stream: lean4

[Adam Topaz]

Is it just me or does copying code blocks from an alectryon documentation result in some crazy additional whitespace?
E.g. copying the first code block from here: https://leanprover.github.io/lean4/doc/examples/tc.lean.html
results in the following

inductive

Expr where
  |

nat  :

Nat →

Expr
  |

plus :

Expr →

Expr →

Expr
  |

bool :

Bool →

Expr
  |

and  :

Expr →

Expr →

Expr

[Adam Topaz]

I can't imagine this is expected behavior?

[Henrik Böving]

This is expected behavior. Alectryon renders the code as dozens and dozens of small HTML fragments with individual class etc. The newlines themselves are also special HTML fragments. And I guess if your browser thinks it should insert some newlines itself between fragments this is what ends up happening?

[Mario Carneiro]

There are definitely ways to fix this. For example, github code is highlighted but it does not do this

[Mario Carneiro]

it looks like the issue is the inline divs for every conceivable hover

[Mario Carneiro]

setting display: none on class alectryon-type-info-wrapper fixes the issue for me

[Sebastian Ullrich]

Right, but then how do we make them visible? Toggling display seems to break the transition-delay.