We need to get back the "Try It" button when manual is read inside VS code documentation view

[lovettchris]

Current behaviour

The LeanInk code snippets (like those in functors) are all nicely annotated by LeanInk, but in the process we lost support for the TryIt button that pops that snippet up in a VS code text editor so user can play with it.

Suggested behaviour

We need to include the original HTML formatted code in a hidden div somewhere with a classname the javascript can look for so it can add the TryIt button back again.

Reasoning

It's handy.

Additional notes