Save Lean example contexts for later

[david-christiansen]

Right now, Lean example contexts exist in an ephemeral environment extension that contains an environment. This is fine if all the examples exist in a single file, but it doesn't work well if one wants to e.g. have a blog post or book chapter that builds on another one.

Serializing the saved environment to a .olean isn't really a good idea. So I plan to add an option to save the syntax of the commands that gave rise to the environment and export them for replay while rendering the other environment.

This is not great for complex running examples (like in Functional Programming in Lean), though. For that, we need a better solution. It could look like writing the example in an examples file with named commands, as the book's text is now, but extracting them into Verso via metaprogramming rather than regexps. This needs further thought.

[david-christiansen]

#50 at least works around this, and may supersede it. I'll try it on bigger examples and then get back.