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.
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