Stack overflows on large Lean blocks

[david-christiansen]

Elaborating large Lean example blocks can lead to excessive stack usage. This can be fixed by e.g. separating multiple definitions into separate blocks, but it shouldn't be happening. There's probably a deep recursion in SubVerso's highlight generation that needs to become a loop, but I don't have time to investigate right now.