We need to get back the "Try It" button when manual is read inside VS code documentation view
Opened this issue · 0 comments
lovettchris commented
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.