Still need to go back and clean up the developer stuff to properly integrate it. Figured developer tool is an easy please to eat our own dogwood on this one.

Do I understand correctly that this is still WIP?

Only the developer tool tweaks. I think the plugin itself is good.

@egor-rogov Done.

Tests are green: https://travis-ci.org/github/highlightjs/highlight.js/pull_requests

But what are the advantages of using Vue in developer.html, I wonder?

To eat our own dog food. If we support Vue, we might as well use it in developer - even if only as a quick way to get bugs reported if the integration breaks for some reason.

Why do we need vue.js and vue.runtime.js in the repository?

I vendored them for the same reason we vendor jquery - to have a pinned version. Or are you asking why we need both? Technically we could just include the one...

To eat our own dog food

It makes sense, but what if we decide to provide another plugin for some other framework?

It makes sense, but what if we decide to provide another plugin for some other framework?

shrugs Can't solve all the worlds problems in one day. :-) Even if this only helps Vue it's still a benefit IMHO.

What helps Vue is the plugin, not our developer tool. Keeping it simple also makes sense for me, as well as "to eat our own dog food".

I meant it helps Vue indirectly as in gives us another reason to keep the plugin maintained. :-)

@allejo All good?