move Webeditor to a separate github package

[joneugster]

Ideally, all projects should import the Webeditor package, so they get access to #package_version. For this, it needs to be a separate repo.

[Kha]

I know our infrastructure does not support this well yet but especially for # commands that are not supposed to "functionally" be part of a package, it would make more sense to inject them dynamically via --plugin instead of making all packages import them statically.

[joneugster]

I have to read up on --plugin, that's the first time I hear of it, but it sounds like the right thing!

Infrastructure might support it now after this weekend's changes

[joneugster]

https://github.com/hhu-adam/lean4web-tools for now

[joneugster]

To my knowledge the current state is that, using --plugin isn't as easy as anticipated and I'm not aware of any demo or doc that would explain how to do this.

If anybody knows how to dynamically load a command #my_command dynamically via --plugin, I'd be happy to see a short demo!